diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /plugins/btauto | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'plugins/btauto')
-rw-r--r-- | plugins/btauto/Algebra.v | 24 | ||||
-rw-r--r-- | plugins/btauto/g_btauto.mlg (renamed from plugins/btauto/g_btauto.ml4) | 6 | ||||
-rw-r--r-- | plugins/btauto/refl_btauto.ml | 30 |
3 files changed, 38 insertions, 22 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index ee7341a4..f1095fc9 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Omega ROmega. +Require Import Bool PArith DecidableClass Omega Lia. Ltac bool := repeat match goal with @@ -84,9 +84,9 @@ Ltac case_decide := match goal with let H := fresh "H" in define (@decide P D) b H; destruct b; try_decide | [ |- context [Pos.compare ?x ?y] ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia | [ X : context [Pos.compare ?x ?y] |- _ ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia end. Section Definitions. @@ -325,13 +325,13 @@ Qed. Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p. Proof. -intros k l p H; revert l; induction H; constructor; eauto; zify; romega. +intros k l p H; revert l; induction H; constructor; eauto; lia. Qed. Lemma linear_valid_incl : forall k p, linear k p -> valid k p. Proof. intros k p H; induction H; constructor; auto. -eapply valid_le_compat; eauto; zify; romega. +eapply valid_le_compat; eauto; lia. Qed. End Validity. @@ -417,13 +417,13 @@ Qed. Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z <= Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (Pos.max ?x ?y < ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | _ => zify; omega end. Hint Resolve Pos.le_max_r Pos.le_max_l. @@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. now rewrite <- (Pos.max_id i); intuition. destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. - + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega. - + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } @@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. -eapply (valid_le_compat i); [now auto|zify; romega]. +eapply (valid_le_compat i); [now auto|lia]. Qed. Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p. diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg index 3ae0f45c..312ef1e5 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin +} + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto -| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] +| [ "btauto" ] -> { Refl_btauto.Btauto.tac } END diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index a09abfa1..c2bc8c07 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,12 +1,24 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Constr + let contrib_name = "btauto" let init_constant dir s = let find_constant contrib dir s = - Universes.constr_of_global (Coqlib.find_reference contrib dir s) + UnivGen.constr_of_global (Coqlib.find_reference contrib dir s) in find_constant contrib_name dir s -let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) +let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in @@ -106,7 +118,7 @@ module Bool = struct let negb = Lazy.force negb in let rec aux c = match decomp_term sigma c with - | Term.App (head, args) -> + | App (head, args) -> if head === andb && Array.length args = 2 then Andb (aux args.(0), aux args.(1)) else if head === orb && Array.length args = 2 then @@ -116,9 +128,9 @@ module Bool = struct else if head === negb && Array.length args = 1 then Negb (aux args.(0)) else Var (Env.add env c) - | Term.Case (info, r, arg, pats) -> + | Case (info, r, arg, pats) -> let is_bool = - let i = info.Term.ci_ind in + let i = info.ci_ind in Names.eq_ind i (Lazy.force ind) in if is_bool then @@ -176,9 +188,9 @@ module Btauto = struct let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in let var = EConstr.Unsafe.to_constr var in let rec to_list l = match decomp_term (Tacmach.project gl) l with - | Term.App (c, _) + | App (c, _) when c === (Lazy.force CoqList._nil) -> [] - | Term.App (c, [|_; h; t|]) + | App (c, [|_; h; t|]) when c === (Lazy.force CoqList._cons) -> if h === (Lazy.force Bool.trueb) then (true :: to_list t) else if h === (Lazy.force Bool.falseb) then (false :: to_list t) @@ -218,7 +230,7 @@ module Btauto = struct let concl = EConstr.Unsafe.to_constr concl in let t = decomp_term (Tacmach.New.project gl) concl in match t with - | Term.App (c, [|typ; p; _|]) when c === eq -> + | App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in tac @@ -236,7 +248,7 @@ module Btauto = struct let bool = Lazy.force Bool.typ in let t = decomp_term sigma concl in match t with - | Term.App (c, [|typ; tl; tr|]) + | App (c, [|typ; tl; tr|]) when typ === bool && c === eq -> let env = Env.empty () in let fl = Bool.quote env sigma tl in |