aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/cctac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/cctac.ml')
-rw-r--r--plugins/cc/cctac.ml356
1 files changed, 178 insertions, 178 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b5be1cdd89..556e6b48e6 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -51,40 +51,40 @@ let sf_of env sigma c = snd (sort_of env sigma c)
let rec decompose_term env sigma t=
match EConstr.kind sigma (whd env sigma t) with
App (f,args)->
- let tf=decompose_term env sigma f in
- let targs=Array.map (decompose_term env sigma) args in
- Array.fold_left (fun s t->Appli (s,t)) tf targs
+ let tf=decompose_term env sigma f in
+ let targs=Array.map (decompose_term env sigma) args in
+ Array.fold_left (fun s t->Appli (s,t)) tf targs
| Prod (_,a,_b) when noccurn sigma 1 _b ->
- let b = Termops.pop _b in
- let sort_b = sf_of env sigma b in
- let sort_a = sf_of env sigma a in
- Appli(Appli(Product (sort_a,sort_b) ,
- decompose_term env sigma a),
- decompose_term env sigma b)
+ let b = Termops.pop _b in
+ let sort_b = sf_of env sigma b in
+ let sort_a = sf_of env sigma a in
+ Appli(Appli(Product (sort_a,sort_b) ,
+ decompose_term env sigma a),
+ decompose_term env sigma b)
| Construct c ->
- let (((mind,i_ind),i_con),u)= c in
- let u = EInstance.kind sigma u in
- let canon_mind = MutInd.make1 (MutInd.canonical mind) in
- let canon_ind = canon_mind,i_ind in
- let (oib,_)=Global.lookup_inductive (canon_ind) in
+ let (((mind,i_ind),i_con),u)= c in
+ let u = EInstance.kind sigma u in
+ let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+ let canon_ind = canon_mind,i_ind in
+ let (oib,_)=Global.lookup_inductive (canon_ind) in
let nargs=constructor_nallargs env (canon_ind,i_con) in
- Constructor {ci_constr= ((canon_ind,i_con),u);
- ci_arity=nargs;
- ci_nhyps=nargs-oib.mind_nparams}
- | Ind c ->
- let (mind,i_ind),u = c in
- let u = EInstance.kind sigma u in
- let canon_mind = MutInd.make1 (MutInd.canonical mind) in
- let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u)))
- | Const (c,u) ->
- let u = EInstance.kind sigma u in
- let canon_const = Constant.make1 (Constant.canonical c) in
- (Symb (Constr.mkConstU (canon_const,u)))
- | Proj (p, c) ->
+ Constructor {ci_constr= ((canon_ind,i_con),u);
+ ci_arity=nargs;
+ ci_nhyps=nargs-oib.mind_nparams}
+ | Ind c ->
+ let (mind,i_ind),u = c in
+ let u = EInstance.kind sigma u in
+ let canon_mind = MutInd.make1 (MutInd.canonical mind) in
+ let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u)))
+ | Const (c,u) ->
+ let u = EInstance.kind sigma u in
+ let canon_const = Constant.make1 (Constant.canonical c) in
+ (Symb (Constr.mkConstU (canon_const,u)))
+ | Proj (p, c) ->
let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
let p' = Projection.map canon_mind p in
- let c = Retyping.expand_projection env sigma p' c [] in
- decompose_term env sigma c
+ let c = Retyping.expand_projection env sigma p' c [] in
+ decompose_term env sigma c
| _ ->
let t = Termops.strip_outer_cast sigma t in
if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found
@@ -97,33 +97,33 @@ let atom_of_constr env sigma term =
let kot = EConstr.kind sigma wh in
match kot with
App (f,args)->
- if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
- then `Eq (args.(0),
- decompose_term env sigma args.(1),
- decompose_term env sigma args.(2))
- else `Other (decompose_term env sigma term)
+ if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
+ then `Eq (args.(0),
+ decompose_term env sigma args.(1),
+ decompose_term env sigma args.(2))
+ else `Other (decompose_term env sigma term)
| _ -> `Other (decompose_term env sigma term)
let rec pattern_of_constr env sigma c =
match EConstr.kind sigma (whd env sigma c) with
App (f,args)->
- let pf = decompose_term env sigma f in
- let pargs,lrels = List.split
- (Array.map_to_list (pattern_of_constr env sigma) args) in
- PApp (pf,List.rev pargs),
- List.fold_left Int.Set.union Int.Set.empty lrels
+ let pf = decompose_term env sigma f in
+ let pargs,lrels = List.split
+ (Array.map_to_list (pattern_of_constr env sigma) args) in
+ PApp (pf,List.rev pargs),
+ List.fold_left Int.Set.union Int.Set.empty lrels
| Prod (_,a,_b) when noccurn sigma 1 _b ->
- let b = Termops.pop _b in
- let pa,sa = pattern_of_constr env sigma a in
- let pb,sb = pattern_of_constr env sigma b in
- let sort_b = sf_of env sigma b in
- let sort_a = sf_of env sigma a in
- PApp(Product (sort_a,sort_b),
- [pa;pb]),(Int.Set.union sa sb)
+ let b = Termops.pop _b in
+ let pa,sa = pattern_of_constr env sigma a in
+ let pb,sb = pattern_of_constr env sigma b in
+ let sort_b = sf_of env sigma b in
+ let sort_a = sf_of env sigma a in
+ PApp(Product (sort_a,sort_b),
+ [pa;pb]),(Int.Set.union sa sb)
| Rel i -> PVar i,Int.Set.singleton i
| _ ->
- let pf = decompose_term env sigma c in
- PApp (pf,[]),Int.Set.empty
+ let pf = decompose_term env sigma c in
+ PApp (pf,[]),Int.Set.empty
let non_trivial = function
PVar _ -> false
@@ -132,52 +132,52 @@ let non_trivial = function
let patterns_of_constr env sigma nrels term=
let f,args=
try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
- if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
- then
- let patt1,rels1 = pattern_of_constr env sigma args.(1)
- and patt2,rels2 = pattern_of_constr env sigma args.(2) in
- let valid1 =
- if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
- else if non_trivial patt1 then Normal
- else Trivial (EConstr.to_constr sigma args.(0))
- and valid2 =
- if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
- else if non_trivial patt2 then Normal
- else Trivial (EConstr.to_constr sigma args.(0)) in
- if valid1 != Creates_variables
- || valid2 != Creates_variables then
- nrels,valid1,patt1,valid2,patt2
- else raise Not_found
- else raise Not_found
+ if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
+ then
+ let patt1,rels1 = pattern_of_constr env sigma args.(1)
+ and patt2,rels2 = pattern_of_constr env sigma args.(2) in
+ let valid1 =
+ if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
+ else if non_trivial patt1 then Normal
+ else Trivial (EConstr.to_constr sigma args.(0))
+ and valid2 =
+ if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
+ else if non_trivial patt2 then Normal
+ else Trivial (EConstr.to_constr sigma args.(0)) in
+ if valid1 != Creates_variables
+ || valid2 != Creates_variables then
+ nrels,valid1,patt1,valid2,patt2
+ else raise Not_found
+ else raise Not_found
let rec quantified_atom_of_constr env sigma nrels term =
match EConstr.kind sigma (whd_delta env sigma term) with
Prod (id,atom,ff) ->
- if is_global sigma (Lazy.force _False) ff then
- let patts=patterns_of_constr env sigma nrels atom in
- `Nrule patts
- else
+ if is_global sigma (Lazy.force _False) ff then
+ let patts=patterns_of_constr env sigma nrels atom in
+ `Nrule patts
+ else
quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
- | _ ->
- let patts=patterns_of_constr env sigma nrels term in
- `Rule patts
+ | _ ->
+ let patts=patterns_of_constr env sigma nrels term in
+ `Rule patts
let litteral_of_constr env sigma term=
match EConstr.kind sigma (whd_delta env sigma term) with
| Prod (id,atom,ff) ->
- if is_global sigma (Lazy.force _False) ff then
- match (atom_of_constr env sigma atom) with
- `Eq(t,a,b) -> `Neq(t,a,b)
- | `Other(p) -> `Nother(p)
- else
- begin
- try
+ if is_global sigma (Lazy.force _False) ff then
+ match (atom_of_constr env sigma atom) with
+ `Eq(t,a,b) -> `Neq(t,a,b)
+ | `Other(p) -> `Nother(p)
+ else
+ begin
+ try
quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
- with Not_found ->
- `Other (decompose_term env sigma term)
- end
+ with Not_found ->
+ `Other (decompose_term env sigma term)
+ end
| _ ->
- atom_of_constr env sigma term
+ atom_of_constr env sigma term
(* store all equalities from the context *)
@@ -191,38 +191,38 @@ let make_prb gls depth additionnal_terms =
let neg_hyps =ref [] in
List.iter
(fun c ->
- let t = decompose_term env sigma c in
- ignore (add_term state t)) additionnal_terms;
+ let t = decompose_term env sigma c in
+ ignore (add_term state t)) additionnal_terms;
List.iter
(fun decl ->
let id = NamedDecl.get_id decl in
- begin
- let cid=Constr.mkVar id in
- match litteral_of_constr env sigma (NamedDecl.get_type decl) with
- `Eq (t,a,b) -> add_equality state cid a b
- | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
- | `Other ph ->
- List.iter
- (fun (cidn,nh) ->
- add_disequality state (HeqnH (cid,cidn)) ph nh)
- !neg_hyps;
- pos_hyps:=(cid,ph):: !pos_hyps
- | `Nother nh ->
- List.iter
- (fun (cidp,ph) ->
- add_disequality state (HeqnH (cidp,cid)) ph nh)
- !pos_hyps;
- neg_hyps:=(cid,nh):: !neg_hyps
- | `Rule patts -> add_quant state id true patts
- | `Nrule patts -> add_quant state id false patts
- end) (Proofview.Goal.hyps gls);
+ begin
+ let cid=Constr.mkVar id in
+ match litteral_of_constr env sigma (NamedDecl.get_type decl) with
+ `Eq (t,a,b) -> add_equality state cid a b
+ | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
+ | `Other ph ->
+ List.iter
+ (fun (cidn,nh) ->
+ add_disequality state (HeqnH (cid,cidn)) ph nh)
+ !neg_hyps;
+ pos_hyps:=(cid,ph):: !pos_hyps
+ | `Nother nh ->
+ List.iter
+ (fun (cidp,ph) ->
+ add_disequality state (HeqnH (cidp,cid)) ph nh)
+ !pos_hyps;
+ neg_hyps:=(cid,nh):: !neg_hyps
+ | `Rule patts -> add_quant state id true patts
+ | `Nrule patts -> add_quant state id false patts
+ end) (Proofview.Goal.hyps gls);
begin
match atom_of_constr env sigma (pf_concl gls) with
- `Eq (t,a,b) -> add_disequality state Goal a b
- | `Other g ->
- List.iter
- (fun (idp,ph) ->
- add_disequality state (HeqG idp) ph g) !pos_hyps
+ `Eq (t,a,b) -> add_disequality state Goal a b
+ | `Other g ->
+ List.iter
+ (fun (idp,ph) ->
+ add_disequality state (HeqG idp) ph g) !pos_hyps
end;
state
@@ -275,7 +275,7 @@ let assert_before n c =
let refresh_type env evm ty =
Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
- (Some false) env evm ty
+ (Some false) env evm ty
let refresh_universes ty k =
Proofview.Goal.enter begin fun gl ->
@@ -295,60 +295,60 @@ let rec proof_tac p : unit Proofview.tactic =
Ax c -> exact_check (EConstr.of_constr c)
| SymAx c ->
let c = EConstr.of_constr c in
- let l=constr_of_term p.p_lhs and
- r=constr_of_term p.p_rhs in
- refresh_universes (type_of l) (fun typ ->
+ let l=constr_of_term p.p_lhs and
+ r=constr_of_term p.p_rhs in
+ refresh_universes (type_of l) (fun typ ->
app_global _sym_eq [|typ;r;l;c|] exact_check)
| Refl t ->
- let lr = constr_of_term t in
- refresh_universes (type_of lr) (fun typ ->
+ let lr = constr_of_term t in
+ refresh_universes (type_of lr) (fun typ ->
app_global _refl_equal [|typ;constr_of_term t|] exact_check)
| Trans (p1,p2)->
- let t1 = constr_of_term p1.p_lhs and
- t2 = constr_of_term p1.p_rhs and
- t3 = constr_of_term p2.p_rhs in
- refresh_universes (type_of t2) (fun typ ->
- let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
+ let t1 = constr_of_term p1.p_lhs and
+ t2 = constr_of_term p1.p_rhs and
+ t3 = constr_of_term p2.p_rhs in
+ refresh_universes (type_of t2) (fun typ ->
+ let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
| Congr (p1,p2)->
- let tf1=constr_of_term p1.p_lhs
- and tx1=constr_of_term p2.p_lhs
- and tf2=constr_of_term p1.p_rhs
- and tx2=constr_of_term p2.p_rhs in
- refresh_universes (type_of tf1) (fun typf ->
- refresh_universes (type_of tx1) (fun typx ->
- refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
+ let tf1=constr_of_term p1.p_lhs
+ and tx1=constr_of_term p2.p_lhs
+ and tf2=constr_of_term p1.p_rhs
+ and tx2=constr_of_term p2.p_rhs in
+ refresh_universes (type_of tf1) (fun typf ->
+ refresh_universes (type_of tx1) (fun typx ->
+ refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in
- let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
- let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
- let prf =
- app_global_with_holes _trans_eq
- [|typfx;
- mkApp(tf1,[|tx1|]);
- mkApp(tf2,[|tx1|]);
- mkApp(tf2,[|tx2|])|] 2 in
- Tacticals.New.tclTHENS prf
- [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
- Tacticals.New.tclFIRST
- [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
- reflexivity;
+ let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
+ let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
+ let prf =
+ app_global_with_holes _trans_eq
+ [|typfx;
+ mkApp(tf1,[|tx1|]);
+ mkApp(tf2,[|tx1|]);
+ mkApp(tf2,[|tx2|])|] 2 in
+ Tacticals.New.tclTHENS prf
+ [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
+ Tacticals.New.tclFIRST
+ [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
+ reflexivity;
Tacticals.New.tclZEROMSG
- (Pp.str
- "I don't know how to handle dependent equality")]])))
+ (Pp.str
+ "I don't know how to handle dependent equality")]])))
| Inject (prf,cstr,nargs,argind) ->
- let ti=constr_of_term prf.p_lhs in
- let tj=constr_of_term prf.p_rhs in
- let default=constr_of_term p.p_lhs in
- let special=mkRel (1+nargs-argind) in
- refresh_universes (type_of ti) (fun intype ->
+ let ti=constr_of_term prf.p_lhs in
+ let tj=constr_of_term prf.p_rhs in
+ let default=constr_of_term p.p_lhs in
+ let special=mkRel (1+nargs-argind) in
+ refresh_universes (type_of ti) (fun intype ->
refresh_universes (type_of default) (fun outtype ->
let sigma, proj =
build_projection intype cstr special default gl
in
- let injt=
+ let injt=
app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
- Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tacticals.New.tclTHEN injt (proof_tac prf))))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
@@ -371,7 +371,7 @@ let refine_exact_check c =
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c)
end
-let convert_to_goal_tac c t1 t2 p =
+let convert_to_goal_tac c t1 t2 p =
Proofview.Goal.enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let k sort =
@@ -381,7 +381,7 @@ let convert_to_goal_tac c t1 t2 p =
let identity=mkLambda (make_annot (Name x) Sorts.Relevant,sort,mkRel 1) in
let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
- [proof_tac p; endt refine_exact_check]
+ [proof_tac p; endt refine_exact_check]
in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
end
@@ -405,7 +405,7 @@ let discriminate_tac cstru p =
let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
let neweq=app_global _eq [|intype;lhs;rhs|] in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
- (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+ (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
[proof_tac p; Equality.discrHyp hid])
end
@@ -430,13 +430,13 @@ let cc_tactic depth additionnal_terms =
match sol with
None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
| Some reason ->
- debug (fun () -> Pp.str "Goal solved, generating proof ...");
- match reason with
- Discrimination (i,ipac,j,jpac) ->
+ debug (fun () -> Pp.str "Goal solved, generating proof ...");
+ match reason with
+ Discrimination (i,ipac,j,jpac) ->
let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
- let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
- discriminate_tac cstr p
- | Incomplete ->
+ let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+ discriminate_tac cstr p
+ | Incomplete ->
let open Glob_term in
let env = Proofview.Goal.env gl in
let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
@@ -456,20 +456,20 @@ let cc_tactic depth additionnal_terms =
end ++
str " replacing metavariables by arbitrary terms.") in
Tacticals.New.tclFAIL 0 msg
- | Contradiction dis ->
+ | Contradiction dis ->
let env = Proofview.Goal.env gl in
let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
- let ta=term uf dis.lhs and tb=term uf dis.rhs in
- match dis.rule with
- Goal -> proof_tac p
- | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
- | HeqG id ->
+ let ta=term uf dis.lhs and tb=term uf dis.rhs in
+ match dis.rule with
+ Goal -> proof_tac p
+ | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
+ | HeqG id ->
let id = EConstr.of_constr id in
- convert_to_goal_tac id ta tb p
- | HeqnH (ida,idb) ->
+ convert_to_goal_tac id ta tb p
+ | HeqnH (ida,idb) ->
let ida = EConstr.of_constr ida in
let idb = EConstr.of_constr idb in
- convert_to_hyp_tac ida ta idb tb p
+ convert_to_hyp_tac ida ta idb tb p
end
let cc_fail =
@@ -509,21 +509,21 @@ let f_equal =
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
Tacticals.New.tclTHENS
- (mk_eq _eq c1 c2 Tactics.cut)
- [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
+ (mk_eq _eq c1 c2 Tactics.cut)
+ [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
begin match EConstr.kind sigma concl with
| App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
- begin match EConstr.kind sigma t, EConstr.kind sigma t' with
- | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
- let rec cuts i =
- if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
- else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
- in cuts (Array.length v - 1)
- | _ -> Proofview.tclUNIT ()
- end
+ begin match EConstr.kind sigma t, EConstr.kind sigma t' with
+ | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
+ let rec cuts i =
+ if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
+ else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+ in cuts (Array.length v - 1)
+ | _ -> Proofview.tclUNIT ()
+ end
| _ -> Proofview.tclUNIT ()
end
begin function (e, info) -> match e with
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:19:08 +0000