diff options
Diffstat (limited to 'contrib/subtac/test')
-rw-r--r-- | contrib/subtac/test/ListDep.v | 8 | ||||
-rw-r--r-- | contrib/subtac/test/Mutind.v | 17 | ||||
-rw-r--r-- | contrib/subtac/test/euclid.v | 11 | ||||
-rw-r--r-- | contrib/subtac/test/measure.v | 10 | ||||
-rw-r--r-- | contrib/subtac/test/take.v | 38 |
5 files changed, 61 insertions, 23 deletions
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v index 97cef9a5..da612c43 100644 --- a/contrib/subtac/test/ListDep.v +++ b/contrib/subtac/test/ListDep.v @@ -1,6 +1,6 @@ (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import List. -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Set Implicit Arguments. @@ -23,13 +23,13 @@ Section Map_DependentRecursor. Variable f : { x : U | In x l } -> V. Obligations Tactic := unfold sub_list in * ; - subtac_simpl ; intuition. + program_simpl ; intuition. Program Fixpoint map_rec ( l' : list U | sub_list l' l ) { measure length l' } : { r : list V | length r = length l' } := match l' with - nil => nil - | cons x tl => let tl' := map_rec tl in + | nil => nil + | cons x tl => let tl' := map_rec tl in f x :: tl' end. diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v index 0b40ef82..ac49ca96 100644 --- a/contrib/subtac/test/Mutind.v +++ b/contrib/subtac/test/Mutind.v @@ -1,13 +1,20 @@ -Program Fixpoint f (a : nat) : nat := +Require Import List. + +Program Fixpoint f a : { x : nat | x > 0 } := match a with - | 0 => 0 + | 0 => 1 | S a' => g a a' end -with g (a b : nat) { struct b } : nat := +with g a b : { x : nat | x > 0 } := match b with - | 0 => 0 + | 0 => 1 | S b' => f b' end. Check f. -Check g.
\ No newline at end of file +Check g. + + + + + diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index a5a8b85f..501aa798 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -1,20 +1,17 @@ -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Require Import Coq.Arith.Compare_dec. Notation "( x & y )" := (existS _ x y) : core_scope. +Require Import Omega. + 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). -Require Import Omega. - -Obligations. -Solve Obligations using subtac_simpl ; omega. - Next Obligation. - assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega. + assert(b * S q' = b * q' + b) by auto with arith ; omega. Defined. Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q). diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v index 4764037d..4f938f4f 100644 --- a/contrib/subtac/test/measure.v +++ b/contrib/subtac/test/measure.v @@ -2,7 +2,7 @@ Notation "( x & y )" := (@existS _ _ x y) : core_scope. Unset Printing All. Require Import Coq.Arith.Compare_dec. -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Fixpoint size (a : nat) : nat := match a with @@ -10,15 +10,11 @@ Fixpoint size (a : nat) : nat := | S n => S (size n) end. -Program Fixpoint test_measure (a : nat) {measure a size} : nat := +Program Fixpoint test_measure (a : nat) {measure size a} : nat := match a with | S (S n) => S (test_measure n) - | x => x + | 0 | S 0 => a end. -subst. -unfold n0. -auto with arith. -Qed. Check test_measure. Print test_measure.
\ No newline at end of file diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v new file mode 100644 index 00000000..87ab47d6 --- /dev/null +++ b/contrib/subtac/test/take.v @@ -0,0 +1,38 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) +Require Import JMeq. +Require Import List. +Require Import Coq.subtac.Utils. + +Set Implicit Arguments. + +Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := + match n with + | 0 => nil + | S p => + match l with + | cons hd tl => let rest := take tl p in cons hd rest + | nil => ! + end + end. + +Require Import Omega. + +Next Obligation. + intros. + simpl in l0. + apply le_S_n ; exact l0. +Defined. + +Next Obligation. + intros. + destruct_call take ; subtac_simpl. +Defined. + +Next Obligation. + intros. + inversion l0. +Defined. + + + + |