diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrOcamlNatBigInt.v | 2 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOcamlNatInt.v | 2 | ||||
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 3 | ||||
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 6 | ||||
| -rw-r--r-- | plugins/romega/const_omega.ml | 175 | ||||
| -rw-r--r-- | plugins/romega/const_omega.mli | 155 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 148 | ||||
| -rw-r--r-- | plugins/rtauto/Rtauto.v | 229 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 12 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 2 |
18 files changed, 385 insertions, 380 deletions
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 264b48a08..c403f7c5a 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -46,7 +46,7 @@ Extract Constant EqNat.eq_nat_decide => "Big.eq". Extract Constant Peano_dec.eq_nat_dec => "Big.eq". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "Big.compare_case Eq Lt Gt". Extract Constant Compare_dec.leb => "Big.le". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 35af71417..a2f809a0c 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -59,7 +59,7 @@ Extract Inlined Constant EqNat.eq_nat_decide => "(=)". Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "fun n m -> if n=m then Eq else if n<m then Lt else Gt". Extract Inlined Constant Compare_dec.leb => "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 543a37ff8..f066ea462 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -21,6 +21,7 @@ Require Import List. Require Import Bool. Require Import OrderedRing. Require Import Refl. +Require Coq.micromega.Tauto. Set Implicit Arguments. @@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) := | OpLe => (psub lhs rhs ,Strict) :: nil end. -Require Import Coq.micromega.Tauto. +Import Coq.micromega.Tauto. Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 85e2a5b23..c5a09d677 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -30,6 +30,7 @@ Require Export Ncring_initial. Require Export Ncring_tac. Require Export Integral_domain. Require Import DiscrR. +Require Import ZArith. Declare ML Module "nsatz_plugin". @@ -56,9 +57,8 @@ simpl. simpl; cring. Qed. (* adpatation du code de Benjamin aux setoides *) -Require Import ZArith. -Require Export Ring_polynom. -Require Export InitialRing. +Export Ring_polynom. +Export InitialRing. Definition PolZ := Pol Z. Definition PEZ := PExpr Z. diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 0f5417e7d..ad3afafd8 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,15 +7,14 @@ *************************************************************************) open Names -open Constr let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] type result = | Kvar of string - | Kapp of string * constr list - | Kimp of constr * constr + | Kapp of string * EConstr.t list + | Kimp of EConstr.t * EConstr.t | Kufo let meaningful_submodule = [ "Z"; "N"; "Pos" ] @@ -30,9 +29,10 @@ let string_of_global r = in prefix^(Names.Id.to_string (Nametab.basename_of_global r)) -let destructurate t = - let c, args = decompose_app t in - match Constr.kind c, args with +let destructurate sigma t = + let c, args = EConstr.decompose_app sigma t in + let open Constr in + match EConstr.kind sigma c, args with | Const (sp,_), args -> Kapp (string_of_global (Globnames.ConstRef sp), args) | Construct (csp,_) , args -> @@ -45,10 +45,11 @@ let destructurate t = exception DestConstApp -let dest_const_apply t = - let f,args = decompose_app t in +let dest_const_apply sigma t = + let open Constr in + let f,args = EConstr.decompose_app sigma t in let ref = - match Constr.kind f with + match EConstr.kind sigma f with | Const (sp,_) -> Globnames.ConstRef sp | Construct (csp,_) -> Globnames.ConstructRef csp | Ind (isp,_) -> Globnames.IndRef isp @@ -66,10 +67,22 @@ let coq_modules = let bin_module = [["Coq";"Numbers";"BinNums"]] let z_module = [["Coq";"ZArith";"BinInt"]] -let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x -let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x -let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x -let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x +let init_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x +let constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" coq_modules x +let z_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" z_module x +let bin_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) let coq_refl_equal = lazy(init_constant "eq_refl") @@ -130,62 +143,64 @@ let coq_O = lazy(init_constant "O") let rec mk_nat = function | 0 -> Lazy.force coq_O - | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) + | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) (* Lists *) -let mkListConst c = - let r = +let mkListConst c = + let r = Coqlib.coq_reference "" ["Init";"Datatypes"] c - in - let inst = - if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] - else fun _ -> Univ.Instance.empty in - fun u -> mkConstructU (Globnames.destConstructRef r, inst u) + let inst = + if Global.is_polymorphic r then + fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|]) + else + fun _ -> EConstr.EInstance.empty + in + fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u) -let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = mkApp (mkListConst "nil" univ, [|typ|]) +let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = EConstr.mkApp (mkListConst "nil" univ, [|typ|]) let mk_list univ typ l = let rec loop = function | [] -> coq_nil univ typ | (step :: l) -> - mkApp (coq_cons univ typ, [| step; loop l |]) in + EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in loop l -let mk_plist = +let mk_plist = let type1lev = Universes.new_univ_level () in - fun l -> mk_list type1lev mkProp l + fun l -> mk_list type1lev EConstr.mkProp l let mk_list = mk_list Univ.Level.set type parse_term = - | Tplus of constr * constr - | Tmult of constr * constr - | Tminus of constr * constr - | Topp of constr - | Tsucc of constr + | Tplus of EConstr.t * EConstr.t + | Tmult of EConstr.t * EConstr.t + | Tminus of EConstr.t * EConstr.t + | Topp of EConstr.t + | Tsucc of EConstr.t | Tnum of Bigint.bigint | Tother type parse_rel = - | Req of constr * constr - | Rne of constr * constr - | Rlt of constr * constr - | Rle of constr * constr - | Rgt of constr * constr - | Rge of constr * constr + | Req of EConstr.t * EConstr.t + | Rne of EConstr.t * EConstr.t + | Rlt of EConstr.t * EConstr.t + | Rle of EConstr.t * EConstr.t + | Rgt of EConstr.t * EConstr.t + | Rge of EConstr.t * EConstr.t | Rtrue | Rfalse - | Rnot of constr - | Ror of constr * constr - | Rand of constr * constr - | Rimp of constr * constr - | Riff of constr * constr + | Rnot of EConstr.t + | Ror of EConstr.t * EConstr.t + | Rand of EConstr.t * EConstr.t + | Rimp of EConstr.t * EConstr.t + | Riff of EConstr.t * EConstr.t | Rother -let parse_logic_rel c = match destructurate c with +let parse_logic_rel sigma c = match destructurate sigma c with | Kapp("True",[]) -> Rtrue | Kapp("False",[]) -> Rfalse | Kapp("not",[t]) -> Rnot t @@ -211,29 +226,29 @@ let rec mk_positive n = if Bigint.equal n Bigint.one then Lazy.force coq_xH else let (q,r) = Bigint.euclid n Bigint.two in - mkApp + EConstr.mkApp ((if Bigint.equal r Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI), [| mk_positive q |]) let mk_N = function | 0 -> Lazy.force coq_N0 - | n -> mkApp (Lazy.force coq_Npos, + | n -> EConstr.mkApp (Lazy.force coq_Npos, [| mk_positive (Bigint.of_int n) |]) module type Int = sig - val typ : constr Lazy.t - val is_int_typ : Proofview.Goal.t -> constr -> bool - val plus : constr Lazy.t - val mult : constr Lazy.t - val opp : constr Lazy.t - val minus : constr Lazy.t - - val mk : Bigint.bigint -> constr - val parse_term : constr -> parse_term - val parse_rel : Proofview.Goal.t -> constr -> parse_rel + val typ : EConstr.t Lazy.t + val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool + val plus : EConstr.t Lazy.t + val mult : EConstr.t Lazy.t + val opp : EConstr.t Lazy.t + val minus : EConstr.t Lazy.t + + val mk : Bigint.bigint -> EConstr.t + val parse_term : Evd.evar_map -> EConstr.t -> parse_term + val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel (* check whether t is built only with numbers and + * - *) - val get_scalar : constr -> Bigint.bigint option + val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option end module Z : Int = struct @@ -244,9 +259,9 @@ let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") let minus = lazy (z_constant "Z.sub") -let recognize_pos t = +let recognize_pos sigma t = let rec loop t = - let f,l = dest_const_apply t in + let f,l = dest_const_apply sigma t in match Id.to_string f,l with | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) | "xO",[t] -> Bigint.mult Bigint.two (loop t) @@ -255,12 +270,12 @@ let recognize_pos t = in try Some (loop t) with DestConstApp -> None -let recognize_Z t = +let recognize_Z sigma t = try - let f,l = dest_const_apply t in + let f,l = dest_const_apply sigma t in match Id.to_string f,l with - | "Zpos",[t] -> recognize_pos t - | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t) + | "Zpos",[t] -> recognize_pos sigma t + | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma t) | "Z0",[] -> Some Bigint.zero | _ -> None with DestConstApp -> None @@ -268,14 +283,14 @@ let recognize_Z t = let mk_Z n = if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 else if Bigint.is_strictly_pos n then - mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) + EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) else - mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) + EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) let mk = mk_Z -let parse_term t = - match destructurate t with +let parse_term sigma t = + match destructurate sigma t with | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) @@ -283,35 +298,35 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (match recognize_Z t with Some t -> Tnum t | None -> Tother) + (match recognize_Z sigma t with Some t -> Tnum t | None -> Tother) | _ -> Tother let is_int_typ gl t = - Tacmach.New.pf_apply Reductionops.is_conv gl - (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) + Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z) let parse_rel gl t = - match destructurate t with + let sigma = Proofview.Goal.sigma gl in + match destructurate sigma t with | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) - | _ -> parse_logic_rel t + | _ -> parse_logic_rel sigma t -let rec get_scalar t = - match destructurate t with +let rec get_scalar sigma t = + match destructurate sigma t with | Kapp("Z.add", [t1;t2]) -> - Option.lift2 Bigint.add (get_scalar t1) (get_scalar t2) + Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2) | Kapp ("Z.sub",[t1;t2]) -> - Option.lift2 Bigint.sub (get_scalar t1) (get_scalar t2) + Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2) | Kapp ("Z.mul",[t1;t2]) -> - Option.lift2 Bigint.mult (get_scalar t1) (get_scalar t2) - | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar t) - | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar t) - | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar t) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z t + Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2) + | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t) + | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t) + | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t) + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t | _ -> None end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index ecddc55de..64668df00 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -8,117 +8,116 @@ (** Coq objects used in romega *) -open Constr (* from Logic *) -val coq_refl_equal : constr lazy_t -val coq_and : constr lazy_t -val coq_not : constr lazy_t -val coq_or : constr lazy_t -val coq_True : constr lazy_t -val coq_False : constr lazy_t -val coq_I : constr lazy_t +val coq_refl_equal : EConstr.t lazy_t +val coq_and : EConstr.t lazy_t +val coq_not : EConstr.t lazy_t +val coq_or : EConstr.t lazy_t +val coq_True : EConstr.t lazy_t +val coq_False : EConstr.t lazy_t +val coq_I : EConstr.t lazy_t (* from ReflOmegaCore/ZOmega *) -val coq_t_int : constr lazy_t -val coq_t_plus : constr lazy_t -val coq_t_mult : constr lazy_t -val coq_t_opp : constr lazy_t -val coq_t_minus : constr lazy_t -val coq_t_var : constr lazy_t - -val coq_proposition : constr lazy_t -val coq_p_eq : constr lazy_t -val coq_p_leq : constr lazy_t -val coq_p_geq : constr lazy_t -val coq_p_lt : constr lazy_t -val coq_p_gt : constr lazy_t -val coq_p_neq : constr lazy_t -val coq_p_true : constr lazy_t -val coq_p_false : constr lazy_t -val coq_p_not : constr lazy_t -val coq_p_or : constr lazy_t -val coq_p_and : constr lazy_t -val coq_p_imp : constr lazy_t -val coq_p_prop : constr lazy_t - -val coq_s_bad_constant : constr lazy_t -val coq_s_divide : constr lazy_t -val coq_s_not_exact_divide : constr lazy_t -val coq_s_sum : constr lazy_t -val coq_s_merge_eq : constr lazy_t -val coq_s_split_ineq : constr lazy_t - -val coq_direction : constr lazy_t -val coq_d_left : constr lazy_t -val coq_d_right : constr lazy_t - -val coq_e_split : constr lazy_t -val coq_e_extract : constr lazy_t -val coq_e_solve : constr lazy_t - -val coq_interp_sequent : constr lazy_t -val coq_do_omega : constr lazy_t - -val mk_nat : int -> constr -val mk_N : int -> constr +val coq_t_int : EConstr.t lazy_t +val coq_t_plus : EConstr.t lazy_t +val coq_t_mult : EConstr.t lazy_t +val coq_t_opp : EConstr.t lazy_t +val coq_t_minus : EConstr.t lazy_t +val coq_t_var : EConstr.t lazy_t + +val coq_proposition : EConstr.t lazy_t +val coq_p_eq : EConstr.t lazy_t +val coq_p_leq : EConstr.t lazy_t +val coq_p_geq : EConstr.t lazy_t +val coq_p_lt : EConstr.t lazy_t +val coq_p_gt : EConstr.t lazy_t +val coq_p_neq : EConstr.t lazy_t +val coq_p_true : EConstr.t lazy_t +val coq_p_false : EConstr.t lazy_t +val coq_p_not : EConstr.t lazy_t +val coq_p_or : EConstr.t lazy_t +val coq_p_and : EConstr.t lazy_t +val coq_p_imp : EConstr.t lazy_t +val coq_p_prop : EConstr.t lazy_t + +val coq_s_bad_constant : EConstr.t lazy_t +val coq_s_divide : EConstr.t lazy_t +val coq_s_not_exact_divide : EConstr.t lazy_t +val coq_s_sum : EConstr.t lazy_t +val coq_s_merge_eq : EConstr.t lazy_t +val coq_s_split_ineq : EConstr.t lazy_t + +val coq_direction : EConstr.t lazy_t +val coq_d_left : EConstr.t lazy_t +val coq_d_right : EConstr.t lazy_t + +val coq_e_split : EConstr.t lazy_t +val coq_e_extract : EConstr.t lazy_t +val coq_e_solve : EConstr.t lazy_t + +val coq_interp_sequent : EConstr.t lazy_t +val coq_do_omega : EConstr.t lazy_t + +val mk_nat : int -> EConstr.t +val mk_N : int -> EConstr.t (** Precondition: the type of the list is in Set *) -val mk_list : constr -> constr list -> constr -val mk_plist : types list -> types +val mk_list : EConstr.t -> EConstr.t list -> EConstr.t +val mk_plist : EConstr.types list -> EConstr.types (** Analyzing a coq term *) (* The generic result shape of the analysis of a term. One-level depth, except when a number is found *) type parse_term = - Tplus of constr * constr - | Tmult of constr * constr - | Tminus of constr * constr - | Topp of constr - | Tsucc of constr + Tplus of EConstr.t * EConstr.t + | Tmult of EConstr.t * EConstr.t + | Tminus of EConstr.t * EConstr.t + | Topp of EConstr.t + | Tsucc of EConstr.t | Tnum of Bigint.bigint | Tother (* The generic result shape of the analysis of a relation. One-level depth. *) type parse_rel = - Req of constr * constr - | Rne of constr * constr - | Rlt of constr * constr - | Rle of constr * constr - | Rgt of constr * constr - | Rge of constr * constr + Req of EConstr.t * EConstr.t + | Rne of EConstr.t * EConstr.t + | Rlt of EConstr.t * EConstr.t + | Rle of EConstr.t * EConstr.t + | Rgt of EConstr.t * EConstr.t + | Rge of EConstr.t * EConstr.t | Rtrue | Rfalse - | Rnot of constr - | Ror of constr * constr - | Rand of constr * constr - | Rimp of constr * constr - | Riff of constr * constr + | Rnot of EConstr.t + | Ror of EConstr.t * EConstr.t + | Rand of EConstr.t * EConstr.t + | Rimp of EConstr.t * EConstr.t + | Riff of EConstr.t * EConstr.t | Rother (* A module factorizing what we should now about the number representation *) module type Int = sig (* the coq type of the numbers *) - val typ : constr Lazy.t + val typ : EConstr.t Lazy.t (* Is a constr expands to the type of these numbers *) - val is_int_typ : Proofview.Goal.t -> constr -> bool + val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool (* the operations on the numbers *) - val plus : constr Lazy.t - val mult : constr Lazy.t - val opp : constr Lazy.t - val minus : constr Lazy.t + val plus : EConstr.t Lazy.t + val mult : EConstr.t Lazy.t + val opp : EConstr.t Lazy.t + val minus : EConstr.t Lazy.t (* building a coq number *) - val mk : Bigint.bigint -> constr + val mk : Bigint.bigint -> EConstr.t (* parsing a term (one level, except if a number is found) *) - val parse_term : constr -> parse_term + val parse_term : Evd.evar_map -> EConstr.t -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proofview.Goal.t -> constr -> parse_rel + val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : constr -> Bigint.bigint option + val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option end (* Currently, we only use Z numbers *) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 54ff44fbd..d18249784 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,7 +8,6 @@ open Pp open Util -open Constr open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -67,14 +66,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq (it could contains some [Term.Var] but no [Term.Rel]). So no need to lift when breaking or creating arrows. *) type oproposition = - Pequa of constr * oequation (* constr = copy of the Coq formula *) + Pequa of EConstr.t * oequation (* constr = copy of the Coq formula *) | Ptrue | Pfalse | Pnot of oproposition | Por of int * oproposition * oproposition | Pand of int * oproposition * oproposition | Pimp of int * oproposition * oproposition - | Pprop of constr + | Pprop of EConstr.t (* The equations *) and oequation = { @@ -101,9 +100,9 @@ and oequation = { type environment = { (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : constr list; + mutable terms : EConstr.t list; (* La meme chose pour les propositions *) - mutable props : constr list; + mutable props : EConstr.t list; (* Traduction des indices utilisés ici en les indices finaux utilisés par * la tactique Omega après dénombrement des variables utiles *) real_indices : int IntHtbl.t; @@ -185,7 +184,7 @@ let print_env_reification env = | t :: l -> let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in @@ -218,8 +217,8 @@ let display_omega_var i = Printf.sprintf "OV%d" i l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) -let add_reified_atom t env = - try List.index0 Constr.equal t env.terms +let add_reified_atom sigma t env = + try List.index0 (EConstr.eq_constr sigma) t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -236,8 +235,8 @@ let set_reified_atom v t env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) -let add_prop env t = - try List.index0 Constr.equal t env.props +let add_prop sigma env t = + try List.index0 (EConstr.eq_constr sigma) t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -290,7 +289,7 @@ let oformula_of_omega af = in loop af.body -let app f v = mkApp(Lazy.force f,v) +let app f v = EConstr.mkApp(Lazy.force f,v) (* \subsection{Oformula vers COQ reel} *) @@ -347,18 +346,19 @@ let reified_conn = function | Pimp _ -> app coq_p_imp | _ -> assert false -let rec reified_of_oprop env t = match t with +let rec reified_of_oprop sigma env t = match t with | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) -> reified_cmp cmp [| reified_of_formula env t1; reified_of_formula env t2 |] | Ptrue -> Lazy.force coq_p_true | Pfalse -> Lazy.force coq_p_false - | Pnot t -> app coq_p_not [| reified_of_oprop env t |] + | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |] | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) -> - reified_conn t [| reified_of_oprop env t1; reified_of_oprop env t2 |] - | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |] + reified_conn t + [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |] + | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |] -let reified_of_proposition env f = - try reified_of_oprop env f +let reified_of_proposition sigma env f = + try reified_of_oprop sigma env f with reraise -> pprint stderr f; raise reraise let reified_of_eq env (l,r) = @@ -475,28 +475,28 @@ let mkPor i x y = Por (i,x,y) let mkPand i x y = Pand (i,x,y) let mkPimp i x y = Pimp (i,x,y) -let rec oformula_of_constr env t = - match Z.parse_term t with - | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2 - | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2 +let rec oformula_of_constr sigma env t = + match Z.parse_term sigma t with + | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2 + | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2 | Tmult (t1,t2) -> - (match Z.get_scalar t1 with - | Some n -> Omult (Oint n,oformula_of_constr env t2) + (match Z.get_scalar sigma t1 with + | Some n -> Omult (Oint n,oformula_of_constr sigma env t2) | None -> - match Z.get_scalar t2 with - | Some n -> Omult (oformula_of_constr env t1, Oint n) - | None -> Oatom (add_reified_atom t env)) - | Topp t -> Oopp(oformula_of_constr env t) - | Tsucc t -> Oplus(oformula_of_constr env t, Oint one) + match Z.get_scalar sigma t2 with + | Some n -> Omult (oformula_of_constr sigma env t1, Oint n) + | None -> Oatom (add_reified_atom sigma t env)) + | Topp t -> Oopp(oformula_of_constr sigma env t) + | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one) | Tnum n -> Oint n - | Tother -> Oatom (add_reified_atom t env) + | Tother -> Oatom (add_reified_atom sigma t env) -and binop env c t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in +and binop sigma env c t1 t2 = + let t1' = oformula_of_constr sigma env t1 in + let t2' = oformula_of_constr sigma env t2 in c t1' t2' -and binprop env (neg2,depends,origin,path) +and binprop sigma env (neg2,depends,origin,path) add_to_depends neg1 gl c t1 t2 = let i = new_connector_id env in let depends1 = if add_to_depends then Left i::depends else depends in @@ -504,41 +504,41 @@ and binprop env (neg2,depends,origin,path) if add_to_depends then IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; let t1' = - oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in + oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = - oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in + oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in (* On numérote le connecteur dans l'environnement. *) c i t1' t2' -and mk_equation env ctxt c connector t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in +and mk_equation sigma env ctxt c connector t1 t2 = + let t1' = oformula_of_constr sigma env t1 in + let t2' = oformula_of_constr sigma env t2 in (* On ajoute l'equation dans l'environnement. *) let omega = normalize_equation env ctxt connector t1' t2' in add_equation env omega; Pequa (c,omega) -and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = +and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c = match Z.parse_rel gl c with - | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2 - | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2 - | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2 - | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2 - | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2 - | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2 + | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2 + | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2 + | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2 + | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2 + | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2 + | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2 | Rtrue -> Ptrue | Rfalse -> Pfalse | Rnot t -> let ctxt' = (not negated, depends, origin,(O_mono::path)) in - Pnot (oproposition_of_constr env ctxt' gl t) - | Ror (t1,t2) -> binprop env ctxt (not negated) negated gl mkPor t1 t2 - | Rand (t1,t2) -> binprop env ctxt negated negated gl mkPand t1 t2 + Pnot (oproposition_of_constr sigma env ctxt' gl t) + | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2 + | Rand (t1,t2) -> binprop sigma env ctxt negated negated gl mkPand t1 t2 | Rimp (t1,t2) -> - binprop env ctxt (not negated) (not negated) gl mkPimp t1 t2 + binprop sigma env ctxt (not negated) (not negated) gl mkPimp t1 t2 | Riff (t1,t2) -> (* No lifting here, since Omega only works on closed propositions. *) - binprop env ctxt negated negated gl mkPand - (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) + binprop sigma env ctxt negated negated gl mkPand + (EConstr.mkArrow t1 t2) (EConstr.mkArrow t2 t1) | _ -> Pprop c (* Destructuration des hypothèses et de la conclusion *) @@ -553,27 +553,25 @@ let display_gl env t_concl t_lhyps = type defined = Defined | Assumed -let reify_hyp env gl i = +let reify_hyp sigma env gl i = let open Context.Named.Declaration in let ctxt = (false,[],i,[]) in match Tacmach.New.pf_get_hyp i gl with - | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) -> - let d = EConstr.Unsafe.to_constr d in + | LocalDef (_,d,t) when Z.is_int_typ gl t -> let dummy = Lazy.force coq_True in - let p = mk_equation env ctxt dummy Eq (mkVar i) d in + let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in i,Defined,p | LocalDef (_,_,t) | LocalAssum (_,t) -> - let t = EConstr.Unsafe.to_constr t in - let p = oproposition_of_constr env ctxt gl t in + let p = oproposition_of_constr sigma env ctxt gl t in i,Assumed,p let reify_gl env gl = + let sigma = Proofview.Goal.sigma gl in let concl = Tacmach.New.pf_concl gl in - let concl = EConstr.Unsafe.to_constr concl in let hyps = Tacmach.New.pf_ids_of_hyps gl in let ctxt_concl = (true,[],id_concl,[O_mono]) in - let t_concl = oproposition_of_constr env ctxt_concl gl concl in - let t_lhyps = List.map (reify_hyp env gl) hyps in + let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in + let t_lhyps = List.map (reify_hyp sigma env gl) hyps in let () = if !debug then display_gl env t_concl t_lhyps in t_concl, t_lhyps @@ -684,8 +682,7 @@ let rec stated_in_tree = function | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) | Leaf s -> stated_in_trace s.s_trace -let mk_refl t = - EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; t|]) +let mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|] let digest_stated_equations env tree = let do_equation st (vars,gens,eqns,ids) = @@ -775,7 +772,7 @@ let maximize_prop equas c = | t1', t2' -> Pand(i,t1',t2')) | Pimp(i,t1,t2) -> (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (Term.mkArrow p1 p2) (* no lift (closed) *) + | Pprop p1, Pprop p2 -> Pprop (EConstr.mkArrow p1 p2) (* no lift (closed) *) | t1', t2' -> Pimp(i,t1',t2')) | Ptrue -> Pprop (app coq_True [||]) | Pfalse -> Pprop (app coq_False [||]) @@ -852,12 +849,15 @@ let hyp_idx env_hyp i = a O_SUM followed by a O_BAD_CONSTANT *) let sum_bad inv i1 i2 = + let open EConstr in mkApp (Lazy.force coq_s_sum, [| Z.mk Bigint.one; i1; Z.mk (if inv then negone else Bigint.one); i2; mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|]) -let rec reify_trace env env_hyp = function +let rec reify_trace env env_hyp = + let open EConstr in + function | CONSTANT_NOT_NUL(e,_) :: [] | CONSTANT_NEG(e,_) :: [] | CONSTANT_NUL e :: [] -> @@ -958,7 +958,7 @@ l'extraction d'un ensemble minimal de solutions permettant la résolution globale du système et enfin construit la trace qui permet de faire rejouer cette solution par la tactique réflexive. *) -let resolution unsafe env (reified_concl,reified_hyps) systems_list = +let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = if !debug then Printf.printf "\n====================================\n"; let all_solutions = List.mapi (solve_system env) systems_list in let solution_tree = solve_with_constraints all_solutions [] in @@ -1006,15 +1006,15 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = (** The environment [env] (and especially [env.real_indices]) is now ready for the coming reifications: *) let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in - let reified_concl = reified_of_proposition env reified_concl in + let reified_concl = reified_of_proposition sigma env reified_concl in let l_reified_terms = List.map (fun id -> match Id.Map.find id reified_hyps with | Defined,p -> - reified_of_proposition env p, mk_refl (mkVar id) + reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id) | Assumed,p -> - reified_of_proposition env (maximize_prop useful_equa_ids p), + reified_of_proposition sigma env (maximize_prop useful_equa_ids p), EConstr.mkVar id | exception Not_found -> assert false) useful_hypnames @@ -1036,17 +1036,16 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = let decompose_tactic = decompose_tree env context solution_tree in Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >> - Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> + Tactics.convert_concl_no_check reified Term.DEFAULTcast >> + Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> show_goal >> (if unsafe then (* Trust the produced term. Faster, but might fail later at Qed. Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check - (EConstr.of_constr (Lazy.force coq_True)) Term.VMcast + Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast else Tactics.normalise_vm_in_concl) >> - Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) + Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic unsafe = Proofview.Goal.nf_enter begin fun gl -> @@ -1064,7 +1063,8 @@ let total_reflexive_omega_tactic unsafe = List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps in if !debug then display_systems systems_list; - resolution unsafe env (concl,hyps) systems_list + let sigma = Proofview.Goal.sigma gl in + resolution unsafe sigma env (concl,hyps) systems_list with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index db17c0d65..06cdf76b4 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -11,7 +11,7 @@ Require Export List. Require Export Bintree. -Require Import Bool. +Require Import Bool BinPos. Declare ML Module "rtauto_plugin". @@ -98,8 +98,6 @@ match F with | F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) end. -Require Export BinPos. - Ltac wipe := intros;simpl;constructor. Lemma compose0 : @@ -257,122 +255,115 @@ Theorem interp_proof: forall p hyps F gl, check_proof hyps gl p = true -> interp_ctx hyps F [[gl]]. -induction p;intros hyps F gl. - -(* cas Axiom *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f nth_f e;rewrite <- (form_eq_refl e). -apply project with p;trivial. - -(* Cas Arrow_Intro *) -Focus 1. -destruct gl;clean. -simpl;intros. -change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). -apply IHp;try constructor;trivial. - -(* Cas Arrow_Elim *) -Focus 1. -simpl check_proof;case_eq (get p hyps);clean. -intros f ef;case_eq (get p0 hyps);clean. -intros f0 ef0;destruct f0;clean. -case_eq (form_eq f f0_1);clean. -simpl;intros e check_p1. -generalize (project F ef) (project F ef0) -(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); -clear check_p1 IHp p p0 p1 ef ef0. -simpl. -apply compose3. -rewrite (form_eq_refl e). -auto. - -(* cas Arrow_Destruct *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean. -intros check_p1 check_p2. -generalize (project F ef) -(IHp1 (hyps \ f1_2 =>> f2 \ f1_1) -(F_push f1_1 (hyps \ f1_2 =>> f2) - (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). -simpl;apply compose3;auto. - -(* Cas False_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intros _; generalize (project F ef). -apply compose1;apply False_ind. - -(* Cas And_Intro *) -Focus 1. -simpl;destruct gl;clean. -case_eq (check_proof hyps gl1 p1);clean. -intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). -apply compose2 ;simpl;auto. - -(* cas And_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intro check_p;generalize (project F ef) -(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). -simpl;apply compose2;intros [h1 h2];auto. - -(* cas And_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro H;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f1_2 =>> f2) -(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl. -apply compose2;auto. - -(* cas Or_Intro_left *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl1 Hp). -apply compose1;simpl;auto. - -(* cas Or_Intro_right *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl2 Hp). -apply compose1;simpl;auto. - -(* cas Or_elim *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -case_eq (check_proof (hyps \ f1) gl p2);clean. -intros check_p1 check_p2;generalize (project F ef) -(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); -simpl;apply compose3;simpl;intro h;destruct h;auto. - -(* cas Or_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro check_p0;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) -(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) - (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl. -apply compose2;auto. - -(* cas Cut *) -Focus 1. -simpl;case_eq (check_proof hyps f p1);clean. -intros check_p1 check_p2; -generalize (IHp1 hyps F f check_p1) -(IHp2 (hyps\f) (F_push f hyps F) gl check_p2); -simpl; apply compose2;auto. +induction p; intros hyps F gl. + +- (* Axiom *) + simpl;case_eq (get p hyps);clean. + intros f nth_f e;rewrite <- (form_eq_refl e). + apply project with p;trivial. + +- (* Arrow_Intro *) + destruct gl; clean. + simpl; intros. + change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). + apply IHp; try constructor; trivial. + +- (* Arrow_Elim *) + simpl check_proof; case_eq (get p hyps); clean. + intros f ef; case_eq (get p0 hyps); clean. + intros f0 ef0; destruct f0; clean. + case_eq (form_eq f f0_1); clean. + simpl; intros e check_p1. + generalize (project F ef) (project F ef0) + (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); + clear check_p1 IHp p p0 p1 ef ef0. + simpl. + apply compose3. + rewrite (form_eq_refl e). + auto. + +- (* Arrow_Destruct *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2); clean. + intros check_p1 check_p2. + generalize (project F ef) + (IHp1 (hyps \ f1_2 =>> f2 \ f1_1) + (F_push f1_1 (hyps \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). + simpl; apply compose3; auto. + +- (* False_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intros _; generalize (project F ef). + apply compose1; apply False_ind. + +- (* And_Intro *) + simpl; destruct gl; clean. + case_eq (check_proof hyps gl1 p1); clean. + intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). + apply compose2 ; simpl; auto. + +- (* And_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intro check_p; + generalize (project F ef) + (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). + simpl; apply compose2; intros [h1 h2]; auto. + +- (* And_Destruct*) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro H; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f1_2 =>> f2) + (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H); + clear H; simpl. + apply compose2; auto. + +- (* Or_Intro_left *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl1 Hp). + apply compose1; simpl; auto. + +- (* Or_Intro_right *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl2 Hp). + apply compose1; simpl; auto. + +- (* Or_elim *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + case_eq (check_proof (hyps \ f1) gl p2); clean. + intros check_p1 check_p2; + generalize (project F ef) + (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); + simpl; apply compose3; simpl; intro h; destruct h; auto. + +- (* Or_Destruct *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro check_p0; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) + (F_push (f1_1 =>> f2) hyps F)) gl check_p0); + simpl. + apply compose2; auto. + +- (* Cut *) + simpl; case_eq (check_proof hyps f p1); clean. + intros check_p1 check_p2; + generalize (IHp1 hyps F f check_p1) + (IHp2 (hyps\f) (F_push f hyps F) gl check_p2); + simpl; apply compose2; auto. Qed. Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e2ec8d72a..f049963f1 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -460,7 +460,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac -(** Open term to lambda-term coercion {{{ ************************************) +(** Open term to lambda-term coercion *)(* {{{ ************************************) (* This operation takes a goal gl and an open term (sigma, t), and *) (* returns a term t' where all the new evars in sigma are abstracted *) @@ -768,7 +768,7 @@ let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl'))) + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> Proofview.V82.of_tactic @@ -1000,7 +1000,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; @@ -1128,7 +1128,7 @@ let interp_clr sigma = function (** Basic tacticals *) -(** Multipliers {{{ ***********************************************************) +(** Multipliers *)(* {{{ ***********************************************************) (* tactical *) @@ -1168,7 +1168,7 @@ let tclMULT = function let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr)) let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) -(** }}} *) +(* }}} *) (** Generalize tactic *) @@ -1199,7 +1199,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs) let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 7c16e1ba9..2b8f1d540 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -414,6 +414,8 @@ val clr_of_wgen : val unfold : EConstr.t list -> unit Proofview.tactic +val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac + (* New code ****************************************************************) (* To call old code *) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 33ebe26b6..717657a24 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration (** The "case" and "elim" tactic *) -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 7f0b77c9e..57635edac 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -372,8 +372,6 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in let r_n' = pf_abs_cterm gl n r_n in diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 96b6ed295..ac2c78249 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -165,7 +165,7 @@ Require Import ssreflect. (* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *) (* axiom: (x op y) op (inv y) = x for all x, y. *) (* Note that familiar "cancellation" identities like x + y - y = x or *) -(* x - y + x = x are respectively instances of right_loop and rev_right_loop *) +(* x - y + y = x are respectively instances of right_loop and rev_right_loop *) (* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *) (* *) (* - Morphisms for functions and relations: *) @@ -639,6 +639,9 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. +(* Force implicits to use as a view. *) +Prenex Implicits Some_inj. + (* cancellation lemmas for dependent type casts. *) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 70f73c1fe..2bed8b624 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint | [ ] -> [ nohint ] END -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) @@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr let old_tac = V82.tactic -(** Name generation {{{ *******************************************************) +(** Name generation *)(* {{{ *******************************************************) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) @@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag) (* We must not anonymize context names discharged by the "in" tactical. *) -(** Tactical extensions. {{{ **************************************************) +(** Tactical extensions. *)(* {{{ **************************************************) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 21ad6e6ce..9cc4f5cec 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -59,7 +59,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) = | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) let hidden_goal_tag = "the_hidden_goal" @@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl = if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let tclCLAUSES tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else let clr_gens = pf_clauseids gl gens clseq in diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index f37452613..e3941c1c5 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. {{{ ************) +(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************) (* Syntax: *) (* if <term> is <pattern> then ... else ... *) @@ -127,7 +127,7 @@ GEXTEND Gram END (* }}} *) -(** Vernacular commands: Prenex Implicits and Search {{{ **********************) +(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -461,7 +461,7 @@ END (* }}} *) -(** View hint database and View application. {{{ ******************************) +(** View hint database and View application. *)(* {{{ ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 5ed5e47f8..33b18001c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -70,7 +70,7 @@ let _ = Goptions.optwrite = debug } let pp s = !pp_ref s -(** Utils {{{ *****************************************************************) +(** Utils *)(* {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind c with App (f, a) -> f, a | _ -> c, [| |] @@ -179,7 +179,7 @@ let nf_evar sigma c = (* }}} *) -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index cd5676f28..07d0f9757 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -74,7 +74,7 @@ val interp_cpattern : pattern (** The set of occurrences to be matched. The boolean is set to true - * to signal the complement of this set (i.e. {-1 3}) *) + * to signal the complement of this set (i.e. \{-1 3\}) *) type occ = (bool * int list) option (** [subst e p t i]. [i] is the number of binders |