summaryrefslogtreecommitdiff
path: root/tactics/equality.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /tactics/equality.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml503
1 files changed, 257 insertions, 246 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f05c3882..2526c84e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: equality.ml 9010 2006-07-05 07:17:41Z jforest $ *)
+(* $Id: equality.ml 9211 2006-10-05 12:38:33Z letouzey $ *)
open Pp
open Util
@@ -82,34 +82,34 @@ let elimination_sort_of_clause = function
*)
let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
- let ctype = pf_type_of gl c in
+ let ctype = pf_apply get_type_of gl c in
(* A delta-reduction would be here too strong, since it would
break search for a defined setoid relation in head position. *)
let t = snd (decompose_prod (whd_betaiotazeta ctype)) in
let head = if isApp t then fst (destApp t) else t in
- if relation_table_mem head && l = NoBindings then
- general_s_rewrite_clause cls lft2rgt c [] gl
- else
- (* Original code. In particular, [splay_prod] performs delta-reduction. *)
- let env = pf_env gl in
- let sigma = project gl in
- let _,t = splay_prod env sigma t in
- match match_with_equation t with
- | None ->
- if l = NoBindings
- then general_s_rewrite_clause cls lft2rgt c [] gl
- else error "The term provided does not end with an equation"
- | Some (hdcncl,_) ->
- let hdcncls = string_of_inductive hdcncl in
- let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
- let dir = if cls=None then lft2rgt else not lft2rgt in
- let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
- let elim =
- try pf_global gl (id_of_string rwr_thm)
- with Not_found ->
- error ("Cannot find rewrite principle "^rwr_thm)
- in
- general_elim_clause cls (c,l) (elim,NoBindings) gl
+ if relation_table_mem head && l = NoBindings then
+ general_s_rewrite_clause cls lft2rgt c [] gl
+ else
+ (* Original code. In particular, [splay_prod] performs delta-reduction. *)
+ let env = pf_env gl in
+ let sigma = project gl in
+ let _,t = splay_prod env sigma t in
+ match match_with_equation t with
+ | None ->
+ if l = NoBindings
+ then general_s_rewrite_clause cls lft2rgt c [] gl
+ else error "The term provided does not end with an equation"
+ | Some (hdcncl,_) ->
+ let hdcncls = string_of_inductive hdcncl in
+ let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+ let dir = if cls=None then lft2rgt else not lft2rgt in
+ let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+ let elim =
+ try pf_global gl (id_of_string rwr_thm)
+ with Not_found ->
+ error ("Cannot find rewrite principle "^rwr_thm)
+ in
+ general_elim_clause cls (c,l) (elim,NoBindings) gl
let general_rewrite_bindings = general_rewrite_bindings_clause None
let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
@@ -119,36 +119,39 @@ let general_rewrite_bindings_in l2r id =
let general_rewrite_in l2r id c =
general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
-
let general_multi_rewrite l2r c cl =
- let rec do_hyps = function
- | [] -> tclIDTAC
- | ((_,id),_) :: l ->
- tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
- in
- let rec try_do_hyps = function
- | [] -> tclIDTAC
- | id :: l ->
- tclTHENFIRST
- (tclTRY (general_rewrite_bindings_in l2r id c))
- (try_do_hyps l)
- in
if cl.concl_occs <> [] then
- error "The \"at\" syntax isn't available yet for the rewrite tactic"
- else
- tclTHENFIRST
- (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
- (match cl.onhyps with
- | Some l -> do_hyps l
- | None ->
- fun gl ->
- (* try to rewrite in all hypothesis
- (except maybe the rewritten one) *)
- let ids = match kind_of_term (fst c) with
- | Var id -> list_remove id (pf_ids_of_hyps gl)
- | _ -> pf_ids_of_hyps gl
- in try_do_hyps ids gl)
-
+ error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+ else match cl.onhyps with
+ | Some l ->
+ (* If a precise list of locations is given, success is mandatory for
+ each of these locations. *)
+ let rec do_hyps = function
+ | [] -> tclIDTAC
+ | ((_,id),_) :: l ->
+ tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+ in
+ if not cl.onconcl then do_hyps l
+ else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l)
+ | None ->
+ (* Otherwise, if we are told to rewrite in all hypothesis via the
+ syntax "* |-", we fail iff all the different rewrites fail *)
+ let rec do_hyps_atleastonce = function
+ | [] -> (fun gl -> error "Nothing to rewrite.")
+ | id :: l ->
+ tclIFTHENTRYELSEMUST
+ (general_rewrite_bindings_in l2r id c)
+ (do_hyps_atleastonce l)
+ in
+ let do_hyps gl =
+ (* If the term to rewrite is an hypothesis, don't rewrite in itself *)
+ let ids = match kind_of_term (fst c) with
+ | Var id -> list_remove id (pf_ids_of_hyps gl)
+ | _ -> pf_ids_of_hyps gl
+ in do_hyps_atleastonce ids gl
+ in
+ if not cl.onconcl then do_hyps
+ else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps
(* Conditional rewriting, the success of a rewriting is related
to the resolution of the conditions by a given tactic *)
@@ -182,9 +185,14 @@ let rewriteRL_clause = function
tac : Used to prove the equality c1 = c2
gl : goal *)
-let abstract_replace clause c2 c1 unsafe tac gl =
- let t1 = pf_type_of gl c1
- and t2 = pf_type_of gl c2 in
+let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
+ let try_prove_eq =
+ match try_prove_eq_opt with
+ | None -> tclIDTAC
+ | Some tac -> tclTRY (tclCOMPLETE tac)
+ in
+ let t1 = pf_apply get_type_of gl c1
+ and t2 = pf_apply get_type_of gl c2 in
if unsafe or (pf_conv_x gl t1 t2) then
let e = build_coq_eq () in
let sym = build_coq_sym_eq () in
@@ -192,34 +200,28 @@ let abstract_replace clause c2 c1 unsafe tac gl =
tclTHENS (assert_tac false Anonymous eq)
[onLastHyp (fun id ->
tclTHEN
- (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings)))
+ (tclTRY (general_multi_rewrite false (mkVar id,NoBindings) clause))
(clear [id]));
tclFIRST
[assumption;
tclTHEN (apply sym) assumption;
- tclTRY (tclCOMPLETE tac)
+ try_prove_eq
]
] gl
else
error "terms do not have convertible types"
+
+let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
-let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl
-
-let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false tclIDTAC gl
+let replace_in id c2 c1 gl = multi_replace (onHyp id) c2 c1 false None gl
-let replace_by c2 c1 tac gl = abstract_replace None c2 c1 false tac gl
+let replace_by c2 c1 tac gl = multi_replace onConcl c2 c1 false (Some tac) gl
-let replace_in_by id c2 c1 tac gl = abstract_replace (Some id) c2 c1 false tac gl
+let replace_in_by id c2 c1 tac gl = multi_replace (onHyp id) c2 c1 false (Some tac) gl
-
-let new_replace c2 c1 id tac_opt gl =
- let tac =
- match tac_opt with
- | Some tac -> tac
- | _ -> tclIDTAC
- in
- abstract_replace id c2 c1 false tac gl
+let replace_in_clause_maybe_by c2 c1 cl tac_opt gl =
+ multi_replace cl c2 c1 false tac_opt gl
(* End of Eduardo's code. The rest of this file could be improved
using the functions match_with_equation, etc that I defined
@@ -269,24 +271,27 @@ exception DiscrFound of
(constructor * int) list * constructor * constructor
let find_positions env sigma t1 t2 =
- let rec findrec posn t1 t2 =
+ let rec findrec sorts posn t1 t2 =
let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in
let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
match (kind_of_term hd1, kind_of_term hd2) with
| Construct sp1, Construct sp2
when List.length args1 = mis_constructor_nargs_env env sp1
- ->
- (* both sides are fully applied constructors, so either we descend,
- or we can discriminate here. *)
+ ->
+ let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
+ (* both sides are fully applied constructors, so either we descend,
+ or we can discriminate here. *)
if sp1 = sp2 then
+ let nrealargs = constructor_nrealargs env sp1 in
+ let rargs1 = list_lastn nrealargs args1 in
+ let rargs2 = list_lastn nrealargs args2 in
List.flatten
- (list_map2_i
- (fun i arg1 arg2 ->
- findrec ((sp1,i)::posn) arg1 arg2)
- 0 args1 args2)
- else
- raise (DiscrFound(List.rev posn,sp1,sp2))
+ (list_map2_i (fun i -> findrec sorts ((sp1,i)::posn))
+ 0 rargs1 rargs2)
+ else if List.mem InType sorts then (* see build_discriminator *)
+ raise (DiscrFound (List.rev posn,sp1,sp2))
+ else []
| _ ->
let t1_0 = applist (hd1,args1)
@@ -295,14 +300,13 @@ let find_positions env sigma t1 t2 =
[]
else
let ty1_0 = get_type_of env sigma t1_0 in
- match get_sort_family_of env sigma ty1_0 with
- | InSet | InType -> [(List.rev posn,t1_0,t2_0)]
- | InProp -> []
- in
- (try
- Inr(findrec [] t1 t2)
- with DiscrFound (path,c1,c2) ->
- Inl (path,c1,c2))
+ let s = get_sort_family_of env sigma ty1_0 in
+ if List.mem s sorts then [(List.rev posn,t1_0,t2_0)] else [] in
+ try
+ (* Rem: to allow injection on proofs objects, just add InProp *)
+ Inr (findrec [InSet;InType] [] t1 t2)
+ with DiscrFound (path,c1,c2) ->
+ Inl (path,c1,c2)
let discriminable env sigma t1 t2 =
match find_positions env sigma t1 t2 with
@@ -371,6 +375,7 @@ let discriminable env sigma t1 t2 =
the continuation then constructs the case-split.
*)
+
let descend_then sigma env head dirn =
let IndType (indf,_) =
try find_rectype env sigma (get_type_of env sigma head)
@@ -383,9 +388,7 @@ let descend_then sigma env head dirn =
(dirn_nlams,
dirn_env,
(fun dirnval (dfltval,resty) ->
- let arsign,_ = get_arity env indf in
- let depind = build_dependent_inductive env indf in
- let deparsign = (Anonymous,None,depind)::arsign in
+ let deparsign = make_arity_signature env true indf in
let p =
it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
let build_branch i =
@@ -416,7 +419,7 @@ let descend_then sigma env head dirn =
let construct_discriminator sigma env dirn c sort =
let IndType(indf,_) =
- try find_rectype env sigma (type_of env sigma c)
+ try find_rectype env sigma (get_type_of env sigma c)
with Not_found ->
(* one can find Rel(k) in case of dependent constructors
like T := c : (A:Set)A->T and a discrimination
@@ -428,10 +431,8 @@ let construct_discriminator sigma env dirn c sort =
dependent types") in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
- let arsign,arsort = get_arity env indf in
let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
- let depind = build_dependent_inductive env indf in
- let deparsign = (Anonymous,None,depind)::arsign in
+ let deparsign = make_arity_signature env true indf in
let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in
let cstrs = get_constructors env indf in
let build_branch i =
@@ -445,17 +446,22 @@ let construct_discriminator sigma env dirn c sort =
let rec build_discriminator sigma env dirn c sort = function
| [] -> construct_discriminator sigma env dirn c sort
| ((sp,cnum),argnum)::l ->
- let cty = type_of env sigma c in
- let IndType (indf,_) =
- try find_rectype env sigma cty with Not_found -> assert false in
- let (ind,_) = dest_ind_family indf in
- let (mib,mip) = lookup_mind_specif env ind in
- let nparams = mib.mind_nparams in
let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
- let newc = mkRel(cnum_nlams-(argnum-nparams)) in
+ let newc = mkRel(cnum_nlams-argnum) in
let subval = build_discriminator sigma cnum_env dirn newc sort l in
kont subval (build_coq_False (),mkSort (Prop Null))
+(* Note: discrimination could be more clever: if some elimination is
+ not allowed because of a large impredicative constructor in the
+ path (see allowed_sorts in find_positions), the positions could
+ still be discrimated by projecting first instead of putting the
+ discrimination combinator inside the projecting combinator. Example
+ of relevant situation:
+
+ Inductive t:Set := c : forall A:Set, A -> nat -> t.
+ Goal ~ c _ 0 0 = c _ 0 1. intro. discriminate H.
+*)
+
let gen_absurdity id gl =
if is_empty_type (clause_type (onHyp id) gl)
then
@@ -466,12 +472,12 @@ let gen_absurdity id gl =
(* Precondition: eq is leibniz equality
- returns ((eq_elim t t1 P i t2), absurd_term)
- where P=[e:t]discriminator
- absurd_term=False
+ returns ((eq_elim t t1 P i t2), absurd_term)
+ where P=[e:t]discriminator
+ absurd_term=False
*)
-let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
+let discrimination_pf e (t,t1,t2) discriminator lbeq =
let i = build_coq_I () in
let absurd_term = build_coq_False () in
let eq_elim = lbeq.ind in
@@ -479,28 +485,28 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
exception NotDiscriminable
-let discrEq (lbeq,(t,t1,t2)) id gls =
- let sort = pf_type_of gls (pf_concl gls) in
+let eq_baseid = id_of_string "e"
+
+let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort =
+ let e = next_ident_away eq_baseid (ids_of_context env) in
+ let e_env = push_named (e,None,t) env in
+ let discriminator =
+ build_discriminator sigma e_env dirn (mkVar e) sort cpath in
+ let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
+ tclCOMPLETE
+ ((tclTHENS (cut_intro absurd_term)
+ [onLastHyp gen_absurdity;
+ refine (mkApp (pf,[|mkVar id|]))]))
+
+let discrEq (lbeq,(t,t1,t2) as u) id gls =
let sigma = project gls in
let env = pf_env gls in
- (match find_positions env sigma t1 t2 with
- | Inr _ ->
- errorlabstrm "discr" (str" Not a discriminable equality")
- | Inl (cpath, (_,dirn), _) ->
- let e = pf_get_new_id (id_of_string "ee") gls in
- let e_env = push_named (e,None,t) env in
- let discriminator =
- build_discriminator sigma e_env dirn (mkVar e) sort cpath in
- let (pf, absurd_term) =
- discrimination_pf e (t,t1,t2) discriminator lbeq gls
- in
- tclCOMPLETE((tclTHENS (cut_intro absurd_term)
- ([onLastHyp gen_absurdity;
- refine (mkApp (pf, [| mkVar id |]))]))) gls)
-
-let not_found_message id =
- (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++
- str" was not found in the current environment")
+ match find_positions env sigma t1 t2 with
+ | Inr _ ->
+ errorlabstrm "discr" (str" Not a discriminable equality")
+ | Inl (cpath, (_,dirn), _) ->
+ let sort = pf_apply get_type_of gls (pf_concl gls) in
+ discr_positions env sigma u id cpath dirn sort gls
let onEquality tac id gls =
let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
@@ -533,7 +539,7 @@ let discrEverywhere =
tclORELSE
(Tacticals.tryAllClauses discrSimpleClause)
(fun gls ->
- errorlabstrm "DiscrEverywhere" (str" No discriminable equalities"))
+ errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
let discr_tac = function
| None -> discrEverywhere
@@ -723,15 +729,9 @@ let make_iterated_tuple env sigma dflt (z,zty) =
let rec build_injrec sigma env dflt c = function
| [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
| ((sp,cnum),argnum)::l ->
- let cty = type_of env sigma c in
- let (ity,_) = find_mrectype env sigma cty in
- let (mib,mip) = lookup_mind_specif env ity in
- let nparams = mib.mind_nparams in
let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
- let newc = mkRel(cnum_nlams-(argnum-nparams)) in
- let (subval,tuplety,dfltval) =
- build_injrec sigma cnum_env dflt newc l
- in
+ let newc = mkRel(cnum_nlams-argnum) in
+ let (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in
(kont subval (dfltval,tuplety),
tuplety,dfltval)
@@ -739,6 +739,7 @@ let build_injector sigma env dflt c cpath =
let (injcode,resty,_) = build_injrec sigma env dflt c cpath in
(injcode,resty)
+(*
let try_delta_expand env sigma t =
let whdt = whd_betadeltaiota env sigma t in
let rec hd_rec c =
@@ -749,12 +750,39 @@ let try_delta_expand env sigma t =
| _ -> t
in
hd_rec whdt
+*)
(* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it
expands then only when the whdnf has a constructor of an inductive type
in hd position, otherwise delta expansion is not done *)
-let injEq (eq,(t,t1,t2)) id gls =
+let simplify_args env sigma t =
+ (* Quick hack to reduce in arguments of eq only *)
+ match decompose_app t with
+ | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2])
+ | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
+ | _ -> t
+
+let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
+ let e = next_ident_away eq_baseid (ids_of_context env) in
+ let e_env = push_named (e,None,t) env in
+ let injectors =
+ map_succeed
+ (fun (cpath,t1',t2') ->
+ (* arbitrarily take t1' as the injector default value *)
+ let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
+ let injfun = mkNamedLambda e t injbody in
+ let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
+ let ty = simplify_args env sigma (get_type_of env sigma pf) in
+ (pf,ty))
+ posns in
+ if injectors = [] then
+ errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
+ tclMAP
+ (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
+ injectors
+
+let injEq ipats (eq,(t,t1,t2)) id gls =
let sigma = project gls in
let env = pf_env gls in
match find_positions env sigma t1 t2 with
@@ -766,100 +794,38 @@ let injEq (eq,(t,t1,t2)) id gls =
errorlabstrm "Equality.inj"
(str"Nothing to do, it is an equality between convertible terms")
| Inr posns ->
- let e = pf_get_new_id (id_of_string "e") gls in
- let e_env = push_named (e,None,t) env in
- let injectors =
- map_succeed
- (fun (cpath,t1_0,t2_0) ->
- try
- let (injbody,resty) =
- (* take arbitrarily t1_0 as the injector default value *)
- build_injector sigma e_env t1_0 (mkVar e) cpath in
- let injfun = mkNamedLambda e t injbody in
- let _ = type_of env sigma injfun in (injfun,resty)
- with e when catchable_exception e ->
- (* may fail because ill-typed or because of a Prop argument *)
- (* error "find_sigma_data" *)
- failwith "caught")
- posns
- in
- if injectors = [] then
- errorlabstrm "Equality.inj"
- (str "Failed to decompose the equality");
- tclMAP
- (fun (injfun,resty) ->
- let pf = applist(eq.congr,
- [t;resty;injfun;
- try_delta_expand env sigma t1;
- try_delta_expand env sigma t2;
- mkVar id])
- in
- let ty =
- try pf_nf gls (pf_type_of gls pf)
- with
- | UserError("refiner__fail",_) ->
- errorlabstrm "InjClause"
- (str (string_of_id id) ++ str" Not a projectable equality")
- in ((tclTHENS (cut ty) ([tclIDTAC;refine pf]))))
- injectors
+(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
+ let t1 = try_delta_expand env sigma t1 in
+ let t2 = try_delta_expand env sigma t2 in
+*)
+ tclTHEN
+ (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
+ (intros_pattern None ipats)
gls
-let inj = onEquality injEq
+let inj ipats = onEquality (injEq ipats)
-let injClause = function
- | None -> onNegatedEquality injEq
- | Some id -> try_intros_until inj id
+let injClause ipats = function
+ | None -> onNegatedEquality (injEq ipats)
+ | Some id -> try_intros_until (inj ipats) id
-let injConcl gls = injClause None gls
-let injHyp id gls = injClause (Some id) gls
+let injConcl gls = injClause [] None gls
+let injHyp id gls = injClause [] (Some id) gls
-let decompEqThen ntac (lbeq,(t,t1,t2)) id gls =
- let sort = pf_type_of gls (pf_concl gls) in
+let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls =
+ let sort = pf_apply get_type_of gls (pf_concl gls) in
let sigma = project gls in
let env = pf_env gls in
- (match find_positions env sigma t1 t2 with
- | Inl (cpath, (_,dirn), _) ->
- let e = pf_get_new_id (id_of_string "e") gls in
- let e_env = push_named (e,None,t) env in
- let discriminator =
- build_discriminator sigma e_env dirn (mkVar e) sort cpath in
- let (pf, absurd_term) =
- discrimination_pf e (t,t1,t2) discriminator lbeq gls in
- tclCOMPLETE
- ((tclTHENS (cut_intro absurd_term)
- ([onLastHyp gen_absurdity;
- refine (mkApp (pf, [| mkVar id |]))]))) gls
- | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
- ntac 0 gls
- | Inr posns ->
- (let e = pf_get_new_id (id_of_string "e") gls in
- let e_env = push_named (e,None,t) env in
- let injectors =
- map_succeed
- (fun (cpath,t1_0,t2_0) ->
- let (injbody,resty) =
- (* take arbitrarily t1_0 as the injector default value *)
- build_injector sigma e_env t1_0 (mkVar e) cpath in
- let injfun = mkNamedLambda e t injbody in
- try
- let _ = type_of env sigma injfun in (injfun,resty)
- with e when catchable_exception e -> failwith "caught")
- posns
- in
- if injectors = [] then
- errorlabstrm "Equality.decompEqThen"
- (str "Discriminate failed to decompose the equality");
- (tclTHEN
- (tclMAP (fun (injfun,resty) ->
- let pf = applist(lbeq.congr,
- [t;resty;injfun;t1;t2;
- mkVar id]) in
- let ty = pf_nf gls (pf_type_of gls pf) in
- ((tclTHENS (cut ty)
- ([tclIDTAC;refine pf]))))
- (List.rev injectors))
- (ntac (List.length injectors)))
- gls))
+ match find_positions env sigma t1 t2 with
+ | Inl (cpath, (_,dirn), _) ->
+ discr_positions env sigma u id cpath dirn sort gls
+ | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
+ ntac 0 gls
+ | Inr posns ->
+ tclTHEN
+ (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns))
+ (ntac (List.length posns))
+ gls
let dEqThen ntac = function
| None -> onNegatedEquality (decompEqThen ntac)
@@ -903,7 +869,7 @@ let find_elim sort_of_gl lbeq =
let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
(* find substitution scheme *)
- let eq_elim = find_elim (pf_type_of gls (pf_concl gls)) lbeq in
+ let eq_elim = find_elim (pf_apply get_type_of gls (pf_concl gls)) lbeq in
(* build substitution predicate *)
let p = lambda_create (pf_env gls) (t,body) in
(* apply substitution scheme *)
@@ -1013,7 +979,7 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
let substClause l2r c cls gls =
- let eq = pf_type_of gls c in
+ let eq = pf_apply get_type_of gls c in
tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls
let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
@@ -1147,28 +1113,10 @@ let subst_all gl =
let ids = list_uniquize ids in
subst ids gl
+
(* Rewrite the first assumption for which the condition faildir does not fail
and gives the direction of the rewrite *)
-let rewrite_assumption_cond faildir gl =
- let rec arec = function
- | [] -> error "No such assumption"
- | (id,_,t)::rest ->
- (try let dir = faildir t gl in
- general_rewrite dir (mkVar id) gl
- with Failure _ | UserError _ -> arec rest)
- in arec (pf_hyps gl)
-
-
-let rewrite_assumption_cond_in faildir hyp gl =
- let rec arec = function
- | [] -> error "No such assumption"
- | (id,_,t)::rest ->
- (try let dir = faildir t gl in
- general_rewrite_in dir hyp (mkVar id) gl
- with Failure _ | UserError _ -> arec rest)
- in arec (pf_hyps gl)
-
let cond_eq_term_left c t gl =
try
let (_,x,_) = snd (find_eq_data_decompose t) in
@@ -1189,6 +1137,48 @@ let cond_eq_term c t gl =
else failwith "not convertible"
with PatternMatchingFailure -> failwith "not an equality"
+let rewrite_mutli_assumption_cond cond_eq_term cl gl =
+ let rec arec = function
+ | [] -> error "No such assumption"
+ | (id,_,t) ::rest ->
+ begin
+ try
+ let dir = cond_eq_term t gl in
+ general_multi_rewrite dir (mkVar id,NoBindings) cl gl
+ with | Failure _ | UserError _ -> arec rest
+ end
+ in
+ arec (pf_hyps gl)
+
+let replace_multi_term dir_opt c =
+ let cond_eq_fun =
+ match dir_opt with
+ | None -> cond_eq_term c
+ | Some true -> cond_eq_term_left c
+ | Some false -> cond_eq_term_right c
+ in
+ rewrite_mutli_assumption_cond cond_eq_fun
+
+(* JF. old version
+let rewrite_assumption_cond faildir gl =
+ let rec arec = function
+ | [] -> error "No such assumption"
+ | (id,_,t)::rest ->
+ (try let dir = faildir t gl in
+ general_rewrite dir (mkVar id) gl
+ with Failure _ | UserError _ -> arec rest)
+ in arec (pf_hyps gl)
+
+
+let rewrite_assumption_cond_in faildir hyp gl =
+ let rec arec = function
+ | [] -> error "No such assumption"
+ | (id,_,t)::rest ->
+ (try let dir = faildir t gl in
+ general_rewrite_in dir hyp (mkVar id) gl
+ with Failure _ | UserError _ -> arec rest)
+ in arec (pf_hyps gl)
+
let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
@@ -1200,6 +1190,27 @@ let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
+*)
+
+let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl
+
+let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl
+
+let replace_term t = replace_multi_term None t Tacticals.onConcl
+
+let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp)
+
+let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp)
+
+let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
+
+
+
+
+
+
+
+
-let _ = Setoid_replace.register_replace replace
+let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl -> replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl)
let _ = Setoid_replace.register_general_rewrite general_rewrite