diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 16:55:45 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-26 16:55:45 +0200 |
commit | 3c16cd6919f2f44cf2732e0bcda88b91ddbbbcff (patch) | |
tree | c3a6a32d80626ee232cba2f0d76e8e0d668ae646 | |
parent | 5084ed22cf500f531375df75fb4f00505d593f55 (diff) | |
parent | 39b4d1d31c6446c937164039cac585dbe91b8b29 (diff) | |
download | smtcoq-3c16cd6919f2f44cf2732e0bcda88b91ddbbbcff.tar.gz smtcoq-3c16cd6919f2f44cf2732e0bcda88b91ddbbbcff.zip |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
-rw-r--r-- | src/versions/standard/Tactics_standard.v | 31 | ||||
-rw-r--r-- | unit-tests/Tests_verit_tactics.v | 17 |
2 files changed, 30 insertions, 18 deletions
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v index 468de7a..232ae54 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/versions/standard/Tactics_standard.v @@ -66,25 +66,28 @@ End Test. (** Tactics in bool *) +Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; auto with typeclass_instances. +Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; auto with typeclass_instances. + Tactic Notation "verit_bool" constr(h) := get_hyps ltac:(fun Hs => match Hs with - | Some ?Hs => verit_bool_base (Some (h, Hs)) - | None => verit_bool_base (Some h) + | Some ?Hs => verit_bool_base_auto (Some (h, Hs)) + | None => verit_bool_base_auto (Some h) end; vauto). Tactic Notation "verit_bool" := - get_hyps ltac:(fun Hs => verit_bool_base Hs; vauto). + get_hyps ltac:(fun Hs => verit_bool_base_auto Hs; vauto). Tactic Notation "verit_bool_no_check" constr(h) := get_hyps ltac:(fun Hs => match Hs with - | Some ?Hs => verit_bool_no_check_base (Some (h, Hs)) - | None => verit_bool_no_check_base (Some h) + | Some ?Hs => verit_bool_no_check_base_auto (Some (h, Hs)) + | None => verit_bool_no_check_base_auto (Some h) end; vauto). Tactic Notation "verit_bool_no_check" := - get_hyps ltac:(fun Hs => verit_bool_no_check_base Hs; vauto). + get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto Hs; vauto). (** Tactics in Prop **) @@ -99,8 +102,8 @@ Tactic Notation "verit" constr(h) := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_base (Some (h, Hs)) ] - | None => verit_bool_base (Some h) + [ .. | verit_bool_base_auto (Some (h, Hs)) ] + | None => verit_bool_base_auto (Some h) end; vauto) ] ]. @@ -110,8 +113,8 @@ Tactic Notation "verit" := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_base (Some Hs) ] - | None => verit_bool_base (@None nat) + [ .. | verit_bool_base_auto (Some Hs) ] + | None => verit_bool_base_auto (@None nat) end; vauto) ]. Tactic Notation "verit_no_check" constr(h) := @@ -121,8 +124,8 @@ Tactic Notation "verit_no_check" constr(h) := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base (Some (h, Hs)) ] - | None => verit_bool_no_check_base (Some h) + [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ] + | None => verit_bool_no_check_base_auto (Some h) end; vauto) ] ]. @@ -132,8 +135,8 @@ Tactic Notation "verit_no_check" := match Hs with | Some ?Hs => prop2bool_hyps Hs; - [ .. | verit_bool_no_check_base (Some Hs) ] - | None => verit_bool_no_check_base (@None nat) + [ .. | verit_bool_no_check_base_auto (Some Hs) ] + | None => verit_bool_no_check_base_auto (@None nat) end; vauto) ]. diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index a270fdd..73b59f4 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -500,12 +500,21 @@ Qed. Goal forall (i j:int), (i == j) && (negb (i == j)) = false. Proof using. - verit. auto with typeclass_instances. + verit. Qed. +Goal forall (i j:int), + ~ ((i = j) /\ (~ (i = j))). +Proof using. verit. Qed. + Goal forall i j, (i == j) || (negb (i == j)). Proof using. - verit. auto with typeclass_instances. + verit. +Qed. + +Goal forall (i j:int), (i = j) \/ (~ (i = j)). +Proof using. + verit. Qed. @@ -1153,10 +1162,10 @@ Qed. Section AppliedPolymorphicTypes1. Goal forall (f : option Z -> Z) (a b : Z), implb (Z.eqb a b) (Z.eqb (f (Some a)) (f (Some b))). - Proof. verit. auto with typeclass_instances. Qed. + Proof. verit. Qed. Goal forall (f : option Z -> Z) (a b : Z), a = b -> f (Some a) = f (Some b). - Proof. verit. auto with typeclass_instances. Qed. + Proof. verit. Qed. End AppliedPolymorphicTypes1. |