From 66f68dfa5aac0252563816d3abef9456e8622adf Mon Sep 17 00:00:00 2001 From: QGarchery Date: Tue, 12 Feb 2019 14:52:13 +0100 Subject: Cleaning (#35) Removing tests from the example folder More commentaries in Example.v --- unit-tests/Tests_verit.v | 144 +++++++++++++++++++++++++++++++++++++++++++++-- unit-tests/debug_coq | 73 ------------------------ unit-tests/debug_coq.v | 73 ++++++++++++++++++++++++ 3 files changed, 211 insertions(+), 79 deletions(-) delete mode 100644 unit-tests/debug_coq create mode 100644 unit-tests/debug_coq.v (limited to 'unit-tests') diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 6a22f8e..f374b1b 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -33,11 +33,15 @@ Qed. (* Proof. *) (* intros f g Hf. *) (* verit Hf. *) -(* exists (fun x y => match (x, y) with (Int31.D0, Int31.D0) | (Int31.D1, Int31.D1) => true | _ => false end). *) -(* intros x y; destruct x, y; constructor; try reflexivity; try discriminate. *) -(* exists Int63Native.eqb. *) -(* apply Int63Properties.reflect_eqb. *) -(* Qed. *) +(* -admit. *) +(* (* a proof that there is a decidable equality on digits : *) *) +(* (* exists (fun x y => match (x, y) with (Int31.D0, Int31.D0) +| (Int31.D1, Int31.D1) => true | _ => false end). *) *) +(* (* intros x y; destruct x, y; constructor; try reflexivity; try discriminate. *) *) +(* (* exists Int63Native.eqb. *) *) +(* (* apply Int63Properties.reflect_eqb. *) *) +(* -apply int63_compdec. *) + Open Scope Z_scope. @@ -1178,7 +1182,7 @@ Section mult3. Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3. Add_lemmas mult3_0 mult3_Sn. - Lemma mult3_21 : mult3 4 =? 12. + Lemma mult3_4_12 : mult3 4 =? 12. Proof. verit. Qed. (* slow to verify with standard coq *) Clear_lemmas. @@ -1337,3 +1341,131 @@ Section group. Clear_lemmas. End group. +Section Linear1. + Parameter f : Z -> Z. + Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). + + (* Cuts are not automatically proved when one equality is switched *) + Lemma f_1 : f 1 =? 1. + Proof. + verit_bool f_spec; replace (0 =? f 0) with (f 0 =? 0) by apply Z.eqb_sym; auto. + Qed. +End Linear1. + +Section Linear2. + Parameter g : Z -> Z. + + Axiom g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2). + +(* The call to veriT does not terminate *) +(* Lemma apply_lemma_infinite : *) +(* forall x y, Z.eqb (g (x + y)) ((g x) + y * 2). *) +(* Proof. verit g_2_linear. *) +End Linear2. + +Section Input_switched1. + Parameter m : Z -> Z. + + Axiom m_0 : m 0 =? 5. + + (* veriT switches the input lemma in this case *) + Lemma cinq_m_0 : m 0 =? 5. + Proof. verit m_0. Qed. +End Input_switched1. + +Section Input_switched2. + Parameter h : Z -> Z -> Z. + + Axiom h_Sm_n : forall x y, h (x+1) y =? h x y. + + (* veriT switches the input lemma in this case *) + Lemma h_1_0 : h 1 0 =? h 0 0. + Proof. verit h_Sm_n. Qed. +End Input_switched2. + + +(** Examples of using the conversion tactics **) + +Local Open Scope positive_scope. + +Goal forall (f : positive -> positive) (x y : positive), + implb ((x + 3) =? y) + ((f (x + 3)) <=? (f y)) + = true. +Proof. +pos_convert. +verit. +Qed. + +Goal forall (f : positive -> positive) (x y : positive), + implb ((x + 3) =? y) + ((3 N) (x y : N), + implb ((x + 3) =? y) + ((f (x + 3)) <=? (f y)) + = true. +Proof. +N_convert. +verit. +Qed. + +Goal forall (f : N -> N) (x y : N), + implb ((x + 3) =? y) + ((2 nat) (x y : nat), + implb (Nat.eqb (x + 3) y) + ((f (x + 3)) <=? (f y)) + = true. +Proof. +nat_convert. +verit. +Qed. + +Goal forall (f : nat -> nat) (x y : nat), + implb (Nat.eqb (x + 3) y) + ((2 nat -> N, forall (x : positive) (y : nat), + implb (x =? 3)%positive + (implb (Nat.eqb y 7) + (implb (f 3%positive 7%nat =? 12)%N + (f x y =? 12)%N)) = true. +pos_convert. +nat_convert. +N_convert. +verit. +Qed. + + +(* The tactic simpl does too much here : *) +(* Goal forall x, 3 + x = x + 3. *) +(* nat_convert. *) diff --git a/unit-tests/debug_coq b/unit-tests/debug_coq deleted file mode 100644 index 61b9fd9..0000000 --- a/unit-tests/debug_coq +++ /dev/null @@ -1,73 +0,0 @@ -(* This file is useful when the tactic goes through but not hte Qed *) -(* It is works as is for standard-coq and checker_b but can be adapted for native-coq and/or checker_eq *) -(* Paste the environment and the following code : *) - - -Definition l := TO_FILL. (* find l in the expression *) -Definition nclauses := let (nclauses, _, _) := c in nclauses. (* different in native-coq *) -Definition confl := let (_, _, confl) := c in confl. (* different in native-coq *) -Definition t := let (_, t, _) := c in t. (* different in native-coq *) - - -Definition nl := Lit.neg l. -Definition d := PArray.make nclauses nl. -Definition s := add_roots (S.make nclauses) d None. - -Compute (checker_b l true c). -Compute (checker (PArray.make nclauses nl) None c). - -Compute (Form.check_form t_form). -Compute (Atom.check_atom t_atom). -Compute (Atom.wt t_i t_func t_atom). -Compute (euf_checker (* t_atom t_form *) C.is_false s t confl). - -(* Check where the false comes from, if its the last one it means the certificate is wring *) -(* To find what rule is causing this, use : *) - - - -Definition flatten {A : Type} (trace : _trace_ A) := - let (t0, _) := t in t0. - -(* INSTEAD in native-coq, use : *) -(* Definition flatten {A : Type} (trace : _trace_ A) := *) -(* PArray.fold_left (fun l_step arr_step => l_step ++ PArray.to_list arr_step) *) -(* nil trace. *) - -Import ListNotations. -Fixpoint firsts {A : Type} (n : nat) (l : list A) := - match n with - | O => [] - | S n => match l with - | [] => [] - | he :: ta => he :: firsts n ta end end. - -Definition step_euf := @step_checker t_i t_func t_atom t_form. -Definition l_t := flatten t. - - -Definition up_to n := List.fold_left step_euf (firsts n l_t) s. -Definition nth n := List.nth (n-1) l_t (ImmBuildProj t_func t_atom t_form 99 99 99). - -Compute (List.length l_t). - - -Compute (up_to 0). -Compute (up_to 1). -Compute (up_to 2). - -Compute (up_to 3). -Compute (up_to 4). -Compute (up_to 5). -Compute (up_to 6). -Compute (nth 6). - -Compute (up_to 7). -Compute (up_to 8). -Compute (up_to 9). -Compute (nth 9). -Compute (up_to 10). -Compute (nth 10). - -Compute (Zpos (xO (xO (xI xH)))). - diff --git a/unit-tests/debug_coq.v b/unit-tests/debug_coq.v new file mode 100644 index 0000000..9ed4b35 --- /dev/null +++ b/unit-tests/debug_coq.v @@ -0,0 +1,73 @@ +(* This file is useful when the tactic goes through but not the Qed *) +(* It is works as is for standard-coq and checker_b but can be adapted for native-coq and/or checker_eq *) +(* Paste the environment and the following code : *) + + +Definition l := TO_FILL. (* find l in the expression *) +Definition nclauses := let (nclauses, _, _) := c in nclauses. (* different in native-coq *) +Definition confl := let (_, _, confl) := c in confl. (* different in native-coq *) +Definition t := let (_, t, _) := c in t. (* different in native-coq *) + + +Definition nl := Lit.neg l. +Definition d := PArray.make nclauses nl. +Definition s := add_roots (S.make nclauses) d None. + +Compute (checker_b l true c). +Compute (checker (PArray.make nclauses nl) None c). + +Compute (Form.check_form t_form). +Compute (Atom.check_atom t_atom). +Compute (Atom.wt t_i t_func t_atom). +Compute (euf_checker (* t_atom t_form *) C.is_false s t confl). + +(* Check where the false comes from, if its the last one it means the certificate is wring *) +(* To find what rule is causing this, use : *) + + + +Definition flatten {A : Type} (trace : _trace_ A) := + let (t0, _) := t in t0. + +(* INSTEAD in native-coq, use : *) +(* Definition flatten {A : Type} (trace : _trace_ A) := *) +(* PArray.fold_left (fun l_step arr_step => l_step ++ PArray.to_list arr_step) *) +(* nil trace. *) + +Import ListNotations. +Fixpoint firsts {A : Type} (n : nat) (l : list A) := + match n with + | O => [] + | S n => match l with + | [] => [] + | he :: ta => he :: firsts n ta end end. + +Definition step_euf := @step_checker t_i t_func t_atom t_form. +Definition l_t := flatten t. + + +Definition up_to n := List.fold_left step_euf (firsts n l_t) s. +Definition nth n := List.nth (n-1) l_t (ImmBuildProj t_func t_atom t_form 99 99 99). + +Compute (List.length l_t). + + +Compute (up_to 0). +Compute (up_to 1). +Compute (up_to 2). + +Compute (up_to 3). +Compute (up_to 4). +Compute (up_to 5). +Compute (up_to 6). +Compute (nth 6). + +Compute (up_to 7). +Compute (up_to 8). +Compute (up_to 9). +Compute (nth 9). +Compute (up_to 10). +Compute (nth 10). + +Compute (Zpos (xO (xO (xI xH)))). + -- cgit