diff options
Diffstat (limited to 'plugins/subtac/test')
-rw-r--r-- | plugins/subtac/test/ListDep.v | 49 | ||||
-rw-r--r-- | plugins/subtac/test/ListsTest.v | 99 | ||||
-rw-r--r-- | plugins/subtac/test/Mutind.v | 20 | ||||
-rw-r--r-- | plugins/subtac/test/Test1.v | 16 | ||||
-rw-r--r-- | plugins/subtac/test/euclid.v | 24 | ||||
-rw-r--r-- | plugins/subtac/test/id.v | 46 | ||||
-rw-r--r-- | plugins/subtac/test/measure.v | 20 | ||||
-rw-r--r-- | plugins/subtac/test/rec.v | 65 | ||||
-rw-r--r-- | plugins/subtac/test/take.v | 34 | ||||
-rw-r--r-- | plugins/subtac/test/wf.v | 48 |
10 files changed, 421 insertions, 0 deletions
diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v new file mode 100644 index 00000000..e3dbd127 --- /dev/null +++ b/plugins/subtac/test/ListDep.v @@ -0,0 +1,49 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) +Require Import List. +Require Import Coq.Program.Program. + +Set Implicit Arguments. + +Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l. + +Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'. +Proof. + intros. + inversion H. + split. + intros. + apply H0. + auto with datatypes. + auto with arith. +Qed. + +Section Map_DependentRecursor. + Variable U V : Set. + Variable l : list U. + Variable f : { x : U | In x l } -> V. + + Obligations Tactic := unfold sub_list in * ; + 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 + f x :: tl' + end. + + Next Obligation. + destruct_call map_rec. + simpl in *. + subst l'. + simpl ; auto with arith. + Qed. + + Program Definition map : list V := map_rec l. + +End Map_DependentRecursor. + +Extraction map. +Extraction map_rec. + diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v new file mode 100644 index 00000000..2cea0841 --- /dev/null +++ b/plugins/subtac/test/ListsTest.v @@ -0,0 +1,99 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) +Require Import Coq.Program.Program. +Require Import List. + +Set Implicit Arguments. + +Section Accessors. + Variable A : Set. + + Program Definition myhd : forall (l : list A | length l <> 0), A := + fun l => + match l with + | nil => ! + | hd :: tl => hd + end. + + Program Definition mytail (l : list A | length l <> 0) : list A := + match l with + | nil => ! + | hd :: tl => tl + end. +End Accessors. + +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 ; program_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 in * ; 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. + + Next Obligation. + Proof. + simpl in *. auto with arith. + Defined. + + Next Obligation. + Proof. + inversion H. + Qed. + + Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := + match l, n with + | hd :: _, 0 => hd + | _ :: tl, S n' => nth' tl n' + | nil, _ => ! + end. + Next Obligation. + Proof. + simpl in *. auto with arith. + Defined. + + Next Obligation. + Proof. + intros. + inversion H. + Defined. + +End Nth. + diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v new file mode 100644 index 00000000..01e2d75f --- /dev/null +++ b/plugins/subtac/test/Mutind.v @@ -0,0 +1,20 @@ +Require Import List. + +Program Fixpoint f a : { x : nat | x > 0 } := + match a with + | 0 => 1 + | S a' => g a a' + end +with g a b : { x : nat | x > 0 } := + match b with + | 0 => 1 + | S b' => f b' + end. + +Check f. +Check g. + + + + + diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v new file mode 100644 index 00000000..7e0755d5 --- /dev/null +++ b/plugins/subtac/test/Test1.v @@ -0,0 +1,16 @@ +Program Definition test (a b : nat) : { x : nat | x = a + b } := + ((a + b) : { x : nat | x = a + b }). +Proof. +intros. +reflexivity. +Qed. + +Print test. + +Require Import List. + +Program hd_opt (l : list nat) : { x : nat | x <> 0 } := + match l with + nil => 1 + | a :: l => a + end. diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v new file mode 100644 index 00000000..97c3d941 --- /dev/null +++ b/plugins/subtac/test/euclid.v @@ -0,0 +1,24 @@ +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). + +Next Obligation. + 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). + +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. diff --git a/plugins/subtac/test/id.v b/plugins/subtac/test/id.v new file mode 100644 index 00000000..9ae11088 --- /dev/null +++ b/plugins/subtac/test/id.v @@ -0,0 +1,46 @@ +Require Coq.Arith.Arith. + +Require Import Coq.subtac.Utils. +Program Fixpoint id (n : nat) : { x : nat | x = n } := + match n with + | O => O + | S p => S (id p) + end. +intros ; auto. + +pose (subset_simpl (id p)). +simpl in e. +unfold p0. +rewrite e. +auto. +Defined. + +Check id. +Print id. +Extraction id. + +Axiom le_gt_dec : forall n m, { n <= m } + { n > m }. +Require Import Omega. + +Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } := + if le_gt_dec n 0 then 0 + else S (id_if (pred n)). +intros. +auto with arith. +intros. +pose (subset_simpl (id_if (pred n))). +simpl in e. +rewrite e. +induction n ; auto with arith. +Defined. + +Print id_if_instance. +Extraction id_if_instance. + +Notation "( x & y )" := (@existS _ _ x y) : core_scope. + +Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} := + (a & a). +intros. +auto. +Qed. diff --git a/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v new file mode 100644 index 00000000..4f938f4f --- /dev/null +++ b/plugins/subtac/test/measure.v @@ -0,0 +1,20 @@ +Notation "( x & y )" := (@existS _ _ x y) : core_scope. +Unset Printing All. +Require Import Coq.Arith.Compare_dec. + +Require Import Coq.Program.Program. + +Fixpoint size (a : nat) : nat := + match a with + 0 => 1 + | S n => S (size n) + end. + +Program Fixpoint test_measure (a : nat) {measure size a} : nat := + match a with + | S (S n) => S (test_measure n) + | 0 | S 0 => a + end. + +Check test_measure. +Print test_measure.
\ No newline at end of file diff --git a/plugins/subtac/test/rec.v b/plugins/subtac/test/rec.v new file mode 100644 index 00000000..aaefd8cc --- /dev/null +++ b/plugins/subtac/test/rec.v @@ -0,0 +1,65 @@ +Require Import Coq.Arith.Arith. +Require Import Lt. +Require Import Omega. + +Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }. +(*Proof. + intros. + elim (le_lt_dec y x) ; intros ; auto with arith. +Defined. +*) +Require Import Coq.subtac.FixSub. +Require Import Wf_nat. + +Lemma preda_lt_a : forall a, 0 < a -> pred a < a. +auto with arith. +Qed. + +Program Fixpoint id_struct (a : nat) : nat := + match a with + 0 => 0 + | S n => S (id_struct n) + end. + +Check struct_rec. + + if (lt_ge_dec O a) + then S (wfrec (pred a)) + else O. + +Program Fixpoint wfrec (a : nat) { wf a lt } : nat := + if (lt_ge_dec O a) + then S (wfrec (pred a)) + else O. +intros. +apply preda_lt_a ; auto. + +Defined. + +Extraction wfrec. +Extraction Inline proj1_sig. +Extract Inductive bool => "bool" [ "true" "false" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. +Extract Inlined Constant lt_ge_dec => "<". + +Extraction wfrec. +Extraction Inline lt_ge_dec le_lt_dec. +Extraction wfrec. + + +Program Fixpoint structrec (a : nat) { wf a lt } : nat := + match a with + S n => S (structrec n) + | 0 => 0 + end. +intros. +unfold n0. +omega. +Defined. + +Print structrec. +Extraction structrec. +Extraction structrec. + +Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a). +Print structrec_fun. diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v new file mode 100644 index 00000000..90ae8bae --- /dev/null +++ b/plugins/subtac/test/take.v @@ -0,0 +1,34 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) +Require Import JMeq. +Require Import List. +Require Import Program. + +Set Implicit Arguments. +Obligations Tactic := idtac. + +Print cons. + +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. +Solve All Obligations. +Next Obligation. + destruct_call take ; program_simpl. +Defined. + +Next Obligation. + intros. + inversion H. +Defined. + + + + diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v new file mode 100644 index 00000000..5ccc154a --- /dev/null +++ b/plugins/subtac/test/wf.v @@ -0,0 +1,48 @@ +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 |