diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/subtac/test/wf.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/subtac/test/wf.v')
-rw-r--r-- | plugins/subtac/test/wf.v | 48 |
1 files changed, 0 insertions, 48 deletions
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v deleted file mode 100644 index 5ccc154a..00000000 --- a/plugins/subtac/test/wf.v +++ /dev/null @@ -1,48 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.subtac.Utils. - -Ltac one_simpl_hyp := - match goal with - | [H : (`exist _ _ _) = _ |- _] => simpl in H - | [H : _ = (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) < _ |- _] => simpl in H - | [H : _ < (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) <= _ |- _] => simpl in H - | [H : _ <= (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) > _ |- _] => simpl in H - | [H : _ > (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) >= _ |- _] => simpl in H - | [H : _ >= (`exist _ _ _) |- _] => simpl in H - end. - -Ltac one_simpl_subtac := - destruct_exists ; - repeat one_simpl_hyp ; simpl. - -Ltac simpl_subtac := do 3 one_simpl_subtac ; simpl. - -Require Import Omega. -Require Import Wf_nat. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). -destruct b ; simpl_subtac. -omega. -simpl_subtac. -assert(x0 * S q' = x0 + x0 * q'). -rewrite <- mult_n_Sm. -omega. -rewrite H2 ; omega. -simpl_subtac. -split ; auto with arith. -omega. -apply lt_wf. -Defined. - -Check euclid_evars_proof.
\ No newline at end of file |