diff options
Diffstat (limited to 'contrib/subtac/test')
-rw-r--r-- | contrib/subtac/test/ListsTest.v | 141 | ||||
-rw-r--r-- | contrib/subtac/test/euclid.v | 73 |
2 files changed, 78 insertions, 136 deletions
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index 8429c267..b8d13fe6 100644 --- a/contrib/subtac/test/ListsTest.v +++ b/contrib/subtac/test/ListsTest.v @@ -1,95 +1,76 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import Coq.subtac.Utils. Require Import List. -Variable A : Set. - -Program Definition myhd : forall { l : list A | length l <> 0 }, A := - fun l => - match `l with - | nil => _ - | hd :: tl => hd - end. -Proof. - destruct l ; simpl ; intro H. - rewrite H in n ; intuition. -Defined. +Set Implicit Arguments. +Section Accessors. + Variable A : Set. -Extraction myhd. -Extraction Inline proj1_sig. + Program Definition myhd : forall { l : list A | length l <> 0 }, A := + fun l => + match l with + | nil => ! + | hd :: tl => hd + end. -Program Definition mytail : forall { l : list A | length l <> 0 }, list A := - fun l => + Program Definition mytail (l : list A | length l <> 0) : list A := match l with - | nil => _ - | hd :: tl => tl + | nil => ! + | hd :: tl => tl end. -Proof. -destruct l ; simpl ; intro H ; rewrite H in n ; intuition. -Defined. - -Extraction mytail. - -Variable a : A. +End Accessors. -Program Definition test_hd : A := myhd (cons a nil). -Proof. -simpl ; auto. -Defined. - -Extraction test_hd. +Program Definition test_hd : nat := myhd (cons 1 nil). +(*Eval compute in test_hd*) (*Program Definition test_tail : list A := mytail nil.*) +Section app. + Variable A : Set. + Program Fixpoint app (l : list A) (l' : list A) { struct l } : + { r : list A | length r = length l + length l' } := + match l with + | nil => l' + | hd :: tl => hd :: (tl ++ l') + end + where "x ++ y" := (app x y). + + Next Obligation. + intros. + destruct_call app ; subtac_simpl. + Defined. + + Program Lemma app_id_l : forall l : list A, l = nil ++ l. + Proof. + simpl ; auto. + Qed. + + Program Lemma app_id_r : forall l : list A, l = l ++ nil. + Proof. + induction l ; simpl ; auto. + rewrite <- IHl ; auto. + Qed. + +End app. + +Extraction app. + +Section Nth. + + Variable A : Set. + + Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := + match n, l with + | 0, hd :: _ => hd + | S n', _ :: tl => nth tl n' + | _, nil => ! + end. - - -Program Fixpoint append (l : list A) (l' : list A) { struct l } : - { r : list A | length r = length l + length l' } := - match l with - | nil => l' - | hd :: tl => hd :: (append tl l') - end. -subst ; auto. -simpl ; rewrite (subset_simpl (append tl0 l')). -simpl ; subst. -simpl ; auto. -Defined. - -Extraction append. - - -Program Lemma append_app' : forall l : list A, l = append nil l. -Proof. -simpl ; auto. -Qed. - -Program Lemma append_app : forall l : list A, l = append l nil. -Proof. -intros. -induction l ; simpl ; auto. -simpl in IHl. -rewrite <- IHl. -reflexivity. -Qed. - - - - - - - - - - - - - - - - - - - + Next Obligation. + Proof. + inversion l0. + Defined. +End Nth. diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index ba5bdf23..a5a8b85f 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -1,66 +1,27 @@ - -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. - -Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) => -@existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a - (@exist nat (fun y : nat => @eq nat a y) a (Evar46 a)). - -Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } := - (a & a). -reflexivity. -Defined. - -Extraction testsig. -Extraction sig. -Extract Inductive sig => "" [ "" ]. -Extraction testsig. - +Require Import Coq.subtac.Utils. Require Import Coq.Arith.Compare_dec. - -Require Import Omega. - -Lemma minus_eq_add : forall x y z w, y <= x -> x - y = y * z + w -> x = y * S z + w. -intros. -assert(y * S z = y * z + y). -auto. -rewrite H1. -omega. -Qed. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : +Notation "( x & y )" := (existS _ x y) : core_scope. + +Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} : { 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). -intro euclid. -simpl ; intros. -Print euclid_evars. -eapply euclid_evars with euclid. -refine (euclid_evars _ _ _ euclid a Acc_a b). -; simpl ; intros. -Show Existentials. -induction b0 ; induction r. -simpl in H. -simpl. -simpl in p0. -destruct p0. -split. +Require Import Omega. + +Obligations. +Solve Obligations using subtac_simpl ; omega. + +Next Obligation. + assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega. +Defined. -apply minus_eq_add. -omega. -auto with arith. -auto. -simpl. -induction b0 ; simpl. -split ; auto. -omega. -exact (euclid a0 Acc_a0 b0). +Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q). -exact (Acc_a). -auto. -auto. -Focus 1. +Eval lazy beta zeta delta iota in test_euclid. +Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } := + (a & S a). +Check testsig. |