aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/blast.ml12
-rw-r--r--contrib/omega/coq_omega.ml45
-rw-r--r--lib/util.ml7
-rw-r--r--lib/util.mli1
-rw-r--r--parsing/pptactic.ml3
-rw-r--r--parsing/q_coqast.ml42
-rw-r--r--pretyping/indrec.ml3
-rw-r--r--pretyping/retyping.ml5
-rw-r--r--tactics/auto.ml30
-rw-r--r--tactics/class_tactics.ml44
-rw-r--r--tactics/eauto.ml44
-rw-r--r--tactics/hipattern.ml4135
-rw-r--r--tactics/hipattern.mli15
-rw-r--r--tactics/tactics.ml35
-rw-r--r--tactics/tactics.mli4
-rw-r--r--tactics/tauto.ml4166
-rw-r--r--theories/Arith/Div2.v62
-rw-r--r--theories/FSets/FSetToFiniteSet.v2
-rw-r--r--theories/Init/Logic.v10
-rw-r--r--theories/Init/Tactics.v12
-rw-r--r--theories/Logic/Decidable.v7
-rw-r--r--theories/NArith/BinNat.v4
22 files changed, 349 insertions, 219 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 189c5360f..483453cb3 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -210,12 +210,12 @@ and e_trivial_resolve db_list local_db gl =
try
priority
(e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl)
+ (fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let e_possible_resolve db_list local_db gl =
try List.map snd (e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl)
+ (fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
@@ -412,7 +412,7 @@ and my_find_search db_list local_db hdc concl =
and trivial_resolve db_list local_db cl =
try
- let hdconstr = List.hd (head_constr_bound cl []) in
+ let hdconstr = fst (head_constr_bound cl) in
priority
(my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
with Bound | Not_found ->
@@ -424,7 +424,7 @@ and trivial_resolve db_list local_db cl =
let possible_resolve db_list local_db cl =
try
- let hdconstr = List.hd (head_constr_bound cl []) in
+ let hdconstr = fst (head_constr_bound cl) in
List.map snd
(my_find_search db_list local_db (head_of_constr_reference hdconstr) cl)
with Bound | Not_found ->
@@ -432,8 +432,8 @@ let possible_resolve db_list local_db cl =
let decomp_unary_term c gls =
let typc = pf_type_of gls c in
- let hd = List.hd (head_constr typc) in
- if Hipattern.is_conjunction hd then
+ let t = head_constr typc in
+ if Hipattern.is_conjunction (applist t) then
simplest_case c gls
else
errorlabstrm "Auto.decomp_unary_term" (str "not a unary type")
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 0bb18b3b0..535459885 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -309,6 +309,7 @@ let coq_dec_True = lazy (constant "dec_True")
let coq_not_or = lazy (constant "not_or")
let coq_not_and = lazy (constant "not_and")
let coq_not_imp = lazy (constant "not_imp")
+let coq_not_iff = lazy (constant "not_iff")
let coq_not_not = lazy (constant "not_not")
let coq_imp_simp = lazy (constant "imp_simp")
let coq_iff = lazy (constant "iff")
@@ -362,7 +363,7 @@ type omega_constant =
| Eq | Neq
| Zne | Zle | Zlt | Zge | Zgt
| Z | Nat
- | And | Or | False | True | Not
+ | And | Or | False | True | Not | Iff
| Le | Lt | Ge | Gt
| Other of string
@@ -388,8 +389,7 @@ let destructurate_prop t =
| _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
| _, [_;_] when c = build_coq_and () -> Kapp (And,args)
| _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
- | _, [t1;t2] when c = Lazy.force coq_iff ->
- Kapp (And,[mkArrow t1 t2;mkArrow t2 t1])
+ | _, [_;_] when c = Lazy.force coq_iff -> Kapp (Iff, args)
| _, [_] when c = build_coq_not () -> Kapp (Not,args)
| _, [] when c = build_coq_False () -> Kapp (False,args)
| _, [] when c = build_coq_True () -> Kapp (True,args)
@@ -1557,6 +1557,9 @@ let rec decidability gl t =
| Kapp(And,[t1;t2]) ->
mkApp (Lazy.force coq_dec_and, [| t1; t2;
decidability gl t1; decidability gl t2 |])
+ | Kapp(Iff,[t1;t2]) ->
+ mkApp (Lazy.force coq_dec_iff, [| t1; t2;
+ decidability gl t1; decidability gl t2 |])
| Kimp(t1,t2) ->
mkApp (Lazy.force coq_dec_imp, [| t1; t2;
decidability gl t1; decidability gl t2 |])
@@ -1620,6 +1623,30 @@ let destructure_hyps gl =
(introduction i2);
(loop ((i1,None,t1)::(i2,None,t2)::lit)) ] gl)
]
+ | Kapp(Iff,[t1;t2]) ->
+ tclTHENLIST [
+ (elim_id i);
+ (tclTRY (clear [i]));
+ (fun gl ->
+ let i1 = fresh_id [] (add_suffix i "_left") gl in
+ let i2 = fresh_id [] (add_suffix i "_right") gl in
+ tclTHENLIST [
+ introduction i1;
+ generalize_tac
+ [mkApp (Lazy.force coq_imp_simp,
+ [| t1; t2; decidability gl t1; mkVar i1|])];
+ onClearedName i1 (fun i1 ->
+ tclTHENLIST [
+ introduction i2;
+ generalize_tac
+ [mkApp (Lazy.force coq_imp_simp,
+ [| t2; t1; decidability gl t2; mkVar i2|])];
+ onClearedName i2 (fun i2 ->
+ loop
+ ((i1,None,mk_or (mk_not t1) t2)::
+ (i2,None,mk_or (mk_not t2) t1)::lit))
+ ])] gl)
+ ]
| Kimp(t1,t2) ->
if
is_Prop (pf_type_of gl t1) &
@@ -1647,10 +1674,20 @@ let destructure_hyps gl =
tclTHENLIST [
(generalize_tac
[mkApp (Lazy.force coq_not_and, [| t1; t2;
- decidability gl t1;mkVar i|])]);
+ decidability gl t1; mkVar i|])]);
(onClearedName i (fun i ->
(loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
]
+ | Kapp(Iff,[t1;t2]) ->
+ tclTHENLIST [
+ (generalize_tac
+ [mkApp (Lazy.force coq_not_iff, [| t1; t2;
+ decidability gl t1; decidability gl t2; mkVar i|])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,
+ mk_or (mk_and t1 (mk_not t2))
+ (mk_and (mk_not t1) t2))::lit))))
+ ]
| Kimp(t1,t2) ->
tclTHENLIST [
(generalize_tac
diff --git a/lib/util.ml b/lib/util.ml
index 3b04e2574..b7aa1fc0e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -946,6 +946,13 @@ let array_for_all4 f v1 v2 v3 v4 =
lv1 = Array.length v4 &&
allrec (pred lv1)
+let array_for_all_i f i v =
+ let rec allrec i = function
+ | -1 -> true
+ | n -> (f i v.(n)) && (allrec (i-1) (n-1))
+ in
+ allrec i ((Array.length v)-1)
+
let array_hd v =
match Array.length v with
| 0 -> failwith "array_hd"
diff --git a/lib/util.mli b/lib/util.mli
index dc6498b15..49e1fb4bd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -196,6 +196,7 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
'a array -> 'b array -> 'c array -> bool
val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
'a array -> 'b array -> 'c array -> 'd array -> bool
+val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
val array_hd : 'a array -> 'a
val array_tl : 'a array -> 'a array
val array_last : 'a array -> 'a
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 78d5cc926..7cb93d108 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -325,9 +325,6 @@ let pr_evaluable_reference_env env = function
| EvalConstRef sp ->
Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp)
-let pr_inductive env ind =
- Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind)
-
let pr_quantified_hypothesis = function
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index fc5df1a6c..18322504e 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -488,6 +488,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
| Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
| Tacexpr.TacArg t ->
<:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >>
+ | Tacexpr.TacComplete t ->
+ <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >>
| _ -> failwith "Quotation of tactic expressions: TODO"
and mlexpr_of_tactic_arg = function
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 996c00eba..689257c3b 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -591,7 +591,8 @@ let lookup_eliminator ind_sp s =
errorlabstrm "default_elim"
(strbrk "Cannot find the elimination combinator " ++
pr_id id ++ strbrk ", the elimination of the inductive definition " ++
- pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++
+ pr_global_env Idset.empty (IndRef ind_sp) ++
+ strbrk " on sort " ++ pr_sort_family s ++
strbrk " is probably not allowed.")
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 123ff43e7..532c258fa 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -115,8 +115,11 @@ let retype sigma metamap =
let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
if Environ.engagement env <> Some ImpredicativeSet &&
s2 = InSet & sort_family_of env t = InType then InType else s2
+ | App(f,args) when isGlobalRef f ->
+ let t = type_of_global_reference_knowing_parameters env f args in
+ family_of_sort (sort_of_atomic_type env sigma t args)
| App(f,args) ->
- family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
+ family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ ->
anomaly "sort_of: Not a type (1)"
| _ -> family_of_sort (decomp_sort env sigma (type_of env t))
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b1e669388..0dd90246d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -279,7 +279,7 @@ let make_exact_entry pri (c,cty) =
let ce = mk_clenv_from dummy_goal (c,cty) in
let c' = clenv_type ce in
let pat = Pattern.pattern_of_constr c' in
- (Some (head_of_constr_reference (List.hd (head_constr cty))),
+ (Some (head_of_constr_reference (fst (head_constr cty))),
{ pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
@@ -352,7 +352,7 @@ let make_extern pri pat tacast =
let make_trivial env sigma c =
let t = hnf_constr env sigma (type_of env sigma c) in
- let hd = head_of_constr_reference (List.hd (head_constr t)) in
+ let hd = head_of_constr_reference (fst (head_constr t)) in
let ce = mk_clenv_from dummy_goal (c,t) in
(Some hd, { pri=1;
pat = Some (Pattern.pattern_of_constr (clenv_type ce));
@@ -412,8 +412,8 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
let subst_key gr =
let (lab'', elab') = subst_global subst gr in
let gr' =
- (try head_of_constr_reference (List.hd (head_constr_bound elab' []))
- with Tactics.Bound -> lab'')
+ (try head_of_constr_reference (fst (head_constr_bound elab'))
+ with Tactics.Bound -> lab'')
in if gr' == gr then gr else gr'
in
let subst_hint (k,data as hint) =
@@ -637,10 +637,7 @@ let print_hint_ref ref = ppnl(pr_hint_ref ref)
let pr_hint_term cl =
try
- let (hdc,args) = match head_constr_bound cl [] with
- | hdc::args -> (hdc,args)
- | [] -> assert false
- in
+ let (hdc,args) = head_constr_bound cl in
let hd = head_of_constr_reference hdc in
let dbs = Hintdbmap.to_list !searchtable in
let valid_dbs =
@@ -864,7 +861,7 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
and trivial_resolve mod_delta db_list local_db cl =
try
- let hdconstr = List.hd (head_constr_bound cl []) in
+ let hdconstr,_ = head_constr_bound cl in
List.map (tac_of_hint db_list local_db cl)
(priority
(my_find_search mod_delta db_list local_db
@@ -906,7 +903,7 @@ let h_trivial lems l =
let possible_resolve mod_delta db_list local_db cl =
try
- let hdconstr = List.hd (head_constr_bound cl []) in
+ let hdconstr,_ = head_constr_bound cl in
List.map (tac_of_hint db_list local_db cl)
(my_find_search mod_delta db_list local_db
(head_of_constr_reference hdconstr) cl)
@@ -915,15 +912,16 @@ let possible_resolve mod_delta db_list local_db cl =
let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
try
- let hd = List.hd (head_constr typc) in
- match Hipattern.match_with_conjunction_size hd with
- | Some (_,_,n) -> tclTHEN (simplest_case (mkVar id)) (kont1 n) gl
- | None -> kont2 gl
+ let ccl = applist (head_constr typc) in
+ match Hipattern.match_with_conjunction ccl with
+ | Some (_,args) ->
+ tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl
+ | None ->
+ kont2 gl
with UserError _ -> kont2 gl
let decomp_empty_term (id,_,typc) gl =
- let (hd,_) = decompose_app typc in
- if Hipattern.is_empty_type hd then
+ if Hipattern.is_empty_type typc then
simplest_case (mkVar id) gl
else
errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 347128921..b556676ee 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -146,13 +146,13 @@ and e_my_find_search db_list local_db hdc concl =
and e_trivial_resolve db_list local_db gl =
try
e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl
+ (fst (head_constr_bound gl)) gl
with Bound | Not_found -> []
let e_possible_resolve db_list local_db gl =
try
e_my_find_search db_list local_db
- (List.hd (head_constr_bound gl [])) gl
+ (fst (head_constr_bound gl)) gl
with Bound | Not_found -> []
let find_first_goal gls =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index dd51acc7b..5e4f847fa 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -198,13 +198,13 @@ and e_trivial_resolve mod_delta db_list local_db gl =
try
priority
(e_my_find_search mod_delta db_list local_db
- (List.hd (head_constr_bound gl [])) gl)
+ (fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let e_possible_resolve mod_delta db_list local_db gl =
try List.map snd
(e_my_find_search mod_delta db_list local_db
- (List.hd (head_constr_bound gl [])) gl)
+ (fst (head_constr_bound gl)) gl)
with Bound | Not_found -> []
let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index c796eda90..769681155 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -15,6 +15,7 @@ open Util
open Names
open Nameops
open Term
+open Sign
open Termops
open Reductionops
open Inductiveops
@@ -64,48 +65,83 @@ let match_with_non_recursive_type t =
let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
-(* A general conjunction type is a non-recursive inductive type with
- only one constructor. *)
+(* Test dependencies *)
-let match_with_conjunction_size t =
- let (hdapp,args) = decompose_app t in
- match kind_of_term hdapp with
- | Ind ind ->
- let (mib,mip) = Global.lookup_inductive ind in
- if (Array.length mip.mind_consnames = 1)
- && (not (mis_is_recursive (ind,mib,mip)))
- && (mip.mind_nrealargs = 0)
- then
- Some (hdapp,args,mip.mind_consnrealdecls.(0))
- else
- None
- | _ -> None
-
-let match_with_conjunction t =
- match match_with_conjunction_size t with
- | Some (hd,args,n) -> Some (hd,args)
- | None -> None
+let rec has_nodep_prod_after n c =
+ match kind_of_term c with
+ | Prod (_,_,b) ->
+ ( n>0 || not (dependent (mkRel 1) b))
+ && (has_nodep_prod_after (n-1) b)
+ | _ -> true
+
+let has_nodep_prod = has_nodep_prod_after 0
-let is_conjunction t = op2bool (match_with_conjunction t)
-
-(* A general disjunction type is a non-recursive inductive type all
- whose constructors have a single argument. *)
+(* A general conjunctive type is a non-recursive with-no-indices inductive
+ type with only one constructor and no dependencies between argument;
+ it is strict if it has the form
+ "Inductive I A1 ... An := C (_:A1) ... (_:An)" *)
-let match_with_disjunction t =
+let match_with_conjunction ?(strict=false) t =
let (hdapp,args) = decompose_app t in
match kind_of_term hdapp with
- | Ind ind ->
- let car = mis_constr_nargs ind in
- if array_for_all (fun ar -> ar = 1) car &&
- (let (mib,mip) = Global.lookup_inductive ind in
- not (mis_is_recursive (ind,mib,mip)))
- then
+ | Ind ind ->
+ let (mib,mip) = Global.lookup_inductive ind in
+ if (Array.length mip.mind_consnames = 1)
+ && (not (mis_is_recursive (ind,mib,mip)))
+ && (mip.mind_nrealargs = 0)
+ then
+ let is_nth_argument n (_,b,c) = b=None && c=mkRel(n+mib.mind_nparams) in
+ if strict &&
+ list_for_all_i is_nth_argument 1
+ (fst (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))
+ then
Some (hdapp,args)
- else
- None
- | _ -> None
+ else
+ let ctyp = prod_applist mip.mind_nf_lc.(0) args in
+ let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in
+ if has_nodep_prod ctyp then
+ Some (hdapp,List.rev cargs)
+ else None
+ else None
+ | _ -> None
+
+let is_conjunction ?(strict=false) t =
+ op2bool (match_with_conjunction ~strict t)
+
+(* A general disjunction type is a non-recursive with-no-indices inductive
+ type with of which all constructors have a single argument;
+ it is strict if it has the form
+ "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
+
+let match_with_disjunction ?(strict=false) t =
+ let (hdapp,args) = decompose_app t in
+ match kind_of_term hdapp with
+ | Ind ind ->
+ let car = mis_constr_nargs ind in
+ let (mib,mip) = Global.lookup_inductive ind in
+ if array_for_all (fun ar -> ar = 1) car &&
+ not (mis_is_recursive (ind,mib,mip))
+ then
+ if strict &
+ array_for_all_i (fun i c ->
+ snd (decompose_prod_n_assum mib.mind_nparams c) = mkRel i) 1
+ mip.mind_nf_lc
+ then
+ Some (hdapp,args)
+ else
+ let cargs =
+ Array.map (fun ar -> pi2 (destProd (prod_applist ar args)))
+ mip.mind_nf_lc in
+ Some (hdapp,Array.to_list cargs)
+ else
+ None
+ | _ -> None
-let is_disjunction t = op2bool (match_with_disjunction t)
+let is_disjunction ?(strict=false) t =
+ op2bool (match_with_disjunction ~strict t)
+
+(* An empty type is an inductive type, possible with indices, that has no
+ constructors *)
let match_with_empty_type t =
let (hdapp,args) = decompose_app t in
@@ -118,22 +154,32 @@ let match_with_empty_type t =
let is_empty_type t = op2bool (match_with_empty_type t)
-let match_with_unit_type t =
+(* This filters inductive types with one constructor with no arguments;
+ Parameters and indices are allowed *)
+
+let match_with_unit_or_eq_type t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
- let zero_args c =
- nb_prod c = mib.mind_nparams in
+ let zero_args c = nb_prod c = mib.mind_nparams in
if nconstr = 1 && zero_args constr_types.(0) then
Some hdapp
- else
+ else
None
| _ -> None
-let is_unit_type t = op2bool (match_with_unit_type t)
+let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
+
+(* A unit type is an inductive type with no indices but possibly
+ (useless) parameters, and that has no constructors *)
+
+let is_unit_type t =
+ match match_with_conjunction t with
+ | Some (_,t) when List.length t = 0 -> true
+ | _ -> false
(* Checks if a given term is an application of an
inductive binary relation R, so that R has only one constructor
@@ -204,15 +250,6 @@ let match_with_imp_term c=
let is_imp_term c = op2bool (match_with_imp_term c)
-let rec has_nodep_prod_after n c =
- match kind_of_term c with
- | Prod (_,_,b) ->
- ( n>0 || not (dependent (mkRel 1) b))
- && (has_nodep_prod_after (n-1) b)
- | _ -> true
-
-let has_nodep_prod = has_nodep_prod_after 0
-
let match_with_nodep_ind t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index a97891c14..b2e25b42d 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -52,19 +52,20 @@ type testing_function = constr -> bool
val match_with_non_recursive_type : (constr * constr list) matching_function
val is_non_recursive_type : testing_function
-val match_with_disjunction : (constr * constr list) matching_function
-val is_disjunction : testing_function
+val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function
+val is_disjunction : ?strict:bool -> testing_function
-val match_with_conjunction : (constr * constr list) matching_function
-val match_with_conjunction_size : (constr * constr list * int) matching_function
-val is_conjunction : testing_function
+val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
+val is_conjunction : ?strict:bool -> testing_function
val match_with_empty_type : constr matching_function
val is_empty_type : testing_function
-val match_with_unit_type : constr matching_function
+(* type with only one constructor and no arguments, possibly with indices *)
+val match_with_unit_or_eq_type : constr matching_function
+val is_unit_or_eq_type : testing_function
-(* type with only one constructor and no arguments *)
+(* type with only one constructor and no arguments, no indices *)
val is_unit_type : testing_function
val match_with_equation : (constr * constr list) matching_function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f06c25a0..c43f829fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -85,15 +85,6 @@ let dloc = dummy_loc
(* General functions *)
(****************************************)
-(*
-let get_pairs_from_bindings =
- let pair_from_binding = function
- | [(Bindings binds)] -> binds
- | _ -> error "not a binding list!"
- in
- List.map pair_from_binding
-*)
-
let string_of_inductive c =
try match kind_of_term c with
| Ind ind_sp ->
@@ -102,26 +93,16 @@ let string_of_inductive c =
| _ -> raise Bound
with Bound -> error "Bound head variable."
-let rec head_constr_bound t l =
- let t = strip_outer_cast(collapse_appl t) in
- match kind_of_term t with
- | Prod (_,_,c2) -> head_constr_bound c2 l
- | LetIn (_,_,_,c2) -> head_constr_bound c2 l
- | App (f,args) ->
- head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
- | Const _ -> t::l
- | Ind _ -> t::l
- | Construct _ -> t::l
- | Var _ -> t::l
- | _ -> raise Bound
+let rec head_constr_bound t =
+ let t = strip_outer_cast t in
+ let _,ccl = decompose_prod_assum t in
+ let hd,args = decompose_app ccl in
+ match kind_of_term hd with
+ | Const _ | Ind _ | Construct _ | Var _ -> (hd,args)
+ | _ -> raise Bound
let head_constr c =
- try head_constr_bound c [] with Bound -> error "Bound head variable."
-
-(*
-let bad_tactic_args s l =
- raise (RefinerError (BadTacticArgs (s,l)))
-*)
+ try head_constr_bound c with Bound -> error "Bound head variable."
(******************************************)
(* Primitive tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 01d517c16..8765541b2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -39,8 +39,8 @@ val inj_ebindings : constr bindings -> open_constr bindings
(*s General functions. *)
val string_of_inductive : constr -> string
-val head_constr : constr -> constr list
-val head_constr_bound : constr -> constr list -> constr list
+val head_constr : constr -> constr * constr list
+val head_constr_bound : constr -> constr * constr list
val is_quantified_hypothesis : identifier -> goal sigma -> bool
exception Bound
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d3dd2959c..3d85f6560 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -21,19 +21,44 @@ open Tacinterp
open Tactics
open Util
-let assoc_last ist =
- match List.assoc (Names.id_of_string "X1") ist.lfun with
+let assoc_var s ist =
+ match List.assoc (Names.id_of_string s) ist.lfun with
| VConstr c -> c
| _ -> failwith "tauto: anomaly"
+(** Parametrization of tauto *)
+
+(* Whether conjunction and disjunction are restricted to binary connectives *)
+(* (this is the compatibility mode) *)
+let binary_mode = true
+
+(* Whether conjunction and disjunction are restricted to the connectives *)
+(* having the structure of "and" and "or" (up to the choice of sorts) in *)
+(* contravariant position in an hypothesis (this is the compatibility mode) *)
+let strict_in_contravariant_hyp = true
+
+(* Whether conjunction and disjunction are restricted to the connectives *)
+(* having the structure of "and" and "or" (up to the choice of sorts) in *)
+(* an hypothesis and in the conclusion *)
+let strict_in_hyp_and_ccl = false
+
+(* Whether unit type includes equality types *)
+let strict_unit = false
+
+
+(** Test *)
+
let is_empty ist =
- if is_empty_type (assoc_last ist) then
+ if is_empty_type (assoc_var "X1" ist) then
<:tactic<idtac>>
else
<:tactic<fail>>
-let is_unit ist =
- if is_unit_type (assoc_last ist) then
+(* Strictly speaking, this exceeds the propositional fragment as it
+ matches also equality types (and solves them if a reflexivity) *)
+let is_unit_or_eq ist =
+ let test = if strict_unit then is_unit_type else is_unit_or_eq_type in
+ if test (assoc_var "X1" ist) then
<:tactic<idtac>>
else
<:tactic<fail>>
@@ -47,93 +72,138 @@ let is_record t =
| _ -> false
let is_binary t =
+ isApp t &&
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
mib.Declarations.mind_nparams = 2
| _ -> false
-
+
+let iter_tac tacl =
+ List.fold_right (fun tac tacs -> <:tactic< $tac; $tacs >>) tacl
+
+(** Dealing with conjunction *)
+
let is_conj ist =
- let ind = assoc_last ist in
- if (is_conjunction ind) && (is_nodep_ind ind) (* && not (is_record ind) *)
- && is_binary ind (* for compatibility, as (?X _ _) matches
- applications with 2 or more arguments. *)
+ let ind = assoc_var "X1" ist in
+ if (not binary_mode || is_binary ind) (* && not (is_record ind) *)
+ && is_conjunction ~strict:strict_in_hyp_and_ccl ind
then
<:tactic<idtac>>
else
<:tactic<fail>>
+let flatten_contravariant_conj ist =
+ let typ = assoc_var "X1" ist in
+ let c = assoc_var "X2" ist in
+ match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
+ | Some (_,args) ->
+ let i = List.length args in
+ if not binary_mode || i = 2 then
+ let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+ let intros =
+ iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
+ <:tactic< idtac >> in
+ <:tactic<
+ let newtyp := $newtyp in
+ assert newtyp by ($intros; apply id; split; assumption);
+ clear id
+ >>
+ else
+ <:tactic<fail>>
+ | _ ->
+ <:tactic<fail>>
+
+(** Dealing with disjunction *)
+
let is_disj ist =
- if is_disjunction (assoc_last ist) && is_binary (assoc_last ist) then
+ let t = assoc_var "X1" ist in
+ if (not binary_mode || is_binary t) &&
+ is_disjunction ~strict:strict_in_hyp_and_ccl t
+ then
<:tactic<idtac>>
else
<:tactic<fail>>
+let flatten_contravariant_disj ist =
+ let typ = assoc_var "X1" ist in
+ let c = assoc_var "X2" ist in
+ match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
+ | Some (_,args) ->
+ let i = List.length args in
+ if not binary_mode || i = 2 then
+ iter_tac (list_map_i (fun i arg ->
+ let typ = valueIn (VConstr (mkArrow arg c)) in
+ <:tactic<
+ let typ := $typ in
+ assert typ by (intro; apply id; constructor $i; assumption)
+ >>) 1 args) <:tactic< clear id >>
+ else
+ <:tactic<fail>>
+ | _ ->
+ <:tactic<fail>>
+
+
+(** Main tactic *)
+
let not_dep_intros ist =
<:tactic<
repeat match goal with
| |- (?X1 -> ?X2) => intro
- | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff
- | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not
- | H:(Coq.Init.Logic.iff _ _)|- _ => unfold Coq.Init.Logic.iff in H
- | H:(Coq.Init.Logic.not _)|-_ => unfold Coq.Init.Logic.not in H
- | H:(Coq.Init.Logic.iff _ _)->_|- _ => unfold Coq.Init.Logic.iff in H
- | H:(Coq.Init.Logic.not _)->_|-_ => unfold Coq.Init.Logic.not in H
+ | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1
+ | H:(Coq.Init.Logic.not _)|-_ => unfold Coq.Init.Logic.not at 1 in H
+ | H:(Coq.Init.Logic.not _)->_|-_ => unfold Coq.Init.Logic.not at 1 in H
end >>
let axioms ist =
- let t_is_unit = tacticIn is_unit
+ let t_is_unit_or_eq = tacticIn is_unit_or_eq
and t_is_empty = tacticIn is_empty in
<:tactic<
match reverse goal with
- | |- ?X1 => $t_is_unit; constructor 1
+ | |- ?X1 => $t_is_unit_or_eq; constructor 1
| _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
| _:?X1 |- ?X1 => assumption
end >>
let simplif ist =
- let t_is_unit = tacticIn is_unit
+ let t_is_unit_or_eq = tacticIn is_unit_or_eq
and t_is_conj = tacticIn is_conj
+ and t_flatten_contravariant_conj = tacticIn flatten_contravariant_conj
+ and t_flatten_contravariant_disj = tacticIn flatten_contravariant_disj
and t_is_disj = tacticIn is_disj
and t_not_dep_intros = tacticIn not_dep_intros in
<:tactic<
$t_not_dep_intros;
repeat
(match reverse goal with
- | id: (?X1 _ _) |- _ =>
- $t_is_conj; elim id; do 2 intro; clear id
- | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id
+ | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id
+ | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
+ | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id
| id0: ?X1-> ?X2, id1: ?X1|- _ =>
(* generalize (id0 id1); intro; clear id0 does not work
(see Marco Maggiesi's bug PR#301)
so we instead use Assert and exact. *)
assert X2; [exact (id0 id1) | clear id0]
| id: ?X1 -> ?X2|- _ =>
- $t_is_unit; cut X2;
+ $t_is_unit_or_eq; cut X2;
[ intro; clear id
| (* id : ?X1 -> ?X2 |- ?X2 *)
cut X1; [exact id| constructor 1; fail]
]
- | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
- $t_is_conj; cut (X2-> X3-> X4);
- [ intro; clear id
- | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X3 -> ?X4 *)
- intro; intro; cut (X1 X2 X3); [exact id| split; assumption]
- ]
- | id: (?X1 ?X2 ?X3) -> ?X4|- _ =>
- $t_is_disj;
- cut (X3-> X4);
- [cut (X2-> X4);
- [intro; intro; clear id
- | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X4 *)
- intro; cut (X1 X2 X3); [exact id| left; assumption]
- ]
- | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X3 -> ?X4 *)
- intro; cut (X1 X2 X3); [exact id| right; assumption]
- ]
- | |- (?X1 _ _) => $t_is_conj; split
+ | id: ?X1 -> ?X2|- _ =>
+ $t_flatten_contravariant_conj
+ (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
+ | id: (Coq.Init.Logic.iff ?X1 ?X2) -> ?X3|- _ =>
+ assert ((X1 -> X2) -> (X2 -> X1) -> X3)
+ by (do 2 intro; apply id; split; assumption);
+ clear id
+ | id: ?X1 -> ?X2|- _ =>
+ $t_flatten_contravariant_disj
+ (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2|-" and "?B->?X2|-" *)
+ | |- ?X1 => $t_is_conj; split
+ | |- (Coq.Init.Logic.iff _ _) => split
end;
$t_not_dep_intros) >>
@@ -153,7 +223,7 @@ let rec tauto_intuit t_reduce solver ist =
[ exact id
| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
solve [ $t_tauto_intuit ]]]
- | |- (?X1 _ _) =>
+ | |- ?X1 =>
$t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit]
end
||
@@ -165,17 +235,17 @@ let rec tauto_intuit t_reduce solver ist =
$t_solver
) >>
-let reduction_not_iff _ist =
+let reduction_not _ist =
<:tactic<repeat
match goal with
- | |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff
- | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H
+ | |- _ => progress unfold Coq.Init.Logic.not
+ | H:_ |- _ => progress unfold Coq.Init.Logic.not in H
end >>
-let t_reduction_not_iff = tacticIn reduction_not_iff
+let t_reduction_not = tacticIn reduction_not
let intuition_gen tac =
- interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
+ interp (tacticIn (tauto_intuit t_reduction_not tac))
let simplif_gen = interp (tacticIn simplif)
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 1f8d13973..4c3b2ff84 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -60,45 +60,38 @@ Hint Resolve lt_div2: arith.
(** Properties related to the parity *)
-Lemma even_odd_div2 :
- forall n,
- (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Lemma even_div2 : forall n, even n -> div2 n = div2 (S n)
+with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
Proof.
- intro n. pattern n in |- *. apply ind_0_1_SS.
- (* n = 0 *)
- split. split; auto with arith.
- split. intro H. inversion H.
- intro H. absurd (S (div2 0) = div2 1); auto with arith.
- (* n = 1 *)
- split. split. intro. inversion H. inversion H1.
- intro H. absurd (div2 1 = div2 2).
- simpl in |- *. discriminate. assumption.
- split; auto with arith.
- (* n = (S (S n')) *)
- intros. decompose [and] H. unfold iff in H0, H1.
- decompose [and] H0. decompose [and] H1. clear H H0 H1.
- split; split; auto with arith.
- intro H. inversion H. inversion H1.
- change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith.
- intro H. inversion H. inversion H1.
- change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith.
+ destruct n; intro H.
+ (* 0 *) trivial.
+ (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial.
+ destruct n; intro.
+ (* 0 *) inversion H.
+ (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
Qed.
-(** Specializations *)
-
-Lemma even_div2 : forall n, even n -> div2 n = div2 (S n).
-Proof fun n => proj1 (proj1 (even_odd_div2 n)).
+Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
+with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Proof.
+ destruct n; intro H.
+ (* 0 *) constructor.
+ (* S n *) constructor. apply div2_odd. rewrite H. trivial.
+ destruct n; intro H.
+ (* 0 *) discriminate.
+ (* S n *) constructor. apply div2_even. injection H as <-. trivial.
+Qed.
-Lemma div2_even : forall n, div2 n = div2 (S n) -> even n.
-Proof fun n => proj2 (proj1 (even_odd_div2 n)).
+Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
-Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
-Proof fun n => proj1 (proj2 (even_odd_div2 n)).
+Lemma even_odd_div2 :
+ forall n,
+ (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Proof.
+ auto decomp using div2_odd, div2_even, odd_div2, even_div2.
+Qed.
-Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
-Proof fun n => proj2 (proj2 (even_odd_div2 n)).
-Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
(** Properties related to the double ([2n]) *)
@@ -132,8 +125,7 @@ Proof.
split; split; auto with arith.
intro H. inversion H. inversion H1.
(* n = (S (S n')) *)
- intros. decompose [and] H. unfold iff in H0, H1.
- decompose [and] H0. decompose [and] H1. clear H H0 H1.
+ intros. destruct H as ((IH1,IH2),(IH3,IH4)).
split; split.
intro H. inversion H. inversion H1.
simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
@@ -142,8 +134,6 @@ Proof.
simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
Qed.
-
-
(** Specializations *)
Lemma even_double : forall n, even n -> n = double (div2 n).
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index 24efa44ef..7938beda7 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -30,7 +30,7 @@ Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
Lemma In_In : forall s x, M.In x s <-> In _ (!!s) x.
Proof.
- unfold In; compute; auto.
+ unfold In; compute; auto with extcore.
Qed.
Lemma Subset_Included : forall s s', s[<=]s' <-> Included _ (!!s) (!!s').
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index b01b80630..a91fd0480 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -150,6 +150,16 @@ Proof.
intros; tauto.
Qed.
+Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
+Proof.
+intros A B []; split; trivial.
+Qed.
+
+Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
+Proof.
+intros; tauto.
+Qed.
+
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
either [P] and [Q], or [~P] and [Q] *)
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 0e8b4ab1f..2e0fe42b6 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -139,18 +139,6 @@ bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
proofs "in one step" *)
Ltac easy :=
-(*
- let rec use_hyp H :=
- match type of H with
- | _ /\ _ =>
- | _ => solve [inversion H]
- end
- with destruct_hyp H :=
- match type of H with
- | _ /\ _ => case H; do_intro; do_intro
- | _ => idtac
- end
-*)
let rec use_hyp H :=
match type of H with
| _ /\ _ => exact H || destruct_hyp H
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 6f793ce2f..6129128de 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -80,6 +80,13 @@ Proof.
unfold decidable; tauto.
Qed.
+Theorem not_iff :
+ forall A B:Prop, decidable A -> decidable B ->
+ ~ (A <-> B) -> (A /\ ~ B) \/ (~ A /\ B).
+Proof.
+unfold decidable; tauto.
+Qed.
+
(** Results formulated with iff, used in FSetDecide.
Negation are expanded since it is unclear whether setoid rewrite
will always perform conversion. *)
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index b704f3d37..d9d848f0d 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -393,10 +393,10 @@ Theorem Ncompare_n_Sm :
Proof.
intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto.
destruct p; simpl; intros; discriminate.
-pose proof (proj1 (Pcompare_p_Sq p q));
+pose proof (Pcompare_p_Sq p q) as (?,_).
assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
intros H; destruct H; discriminate.
-pose proof (proj2 (Pcompare_p_Sq p q));
+pose proof (Pcompare_p_Sq p q) as (_,?);
assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:58:30 +0000