diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 11:04:58 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 11:04:58 +0000 |
commit | 34984f6eb046ad3adc78ebac8ab3e6d0bc08c7cf (patch) | |
tree | ff404a1a28723dd250879698fcf09250bc5ae4ba | |
parent | 1011266b84371b34536dd5aa5afb3a44b8f8d53c (diff) |
Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due to dependencies though.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14672 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tactics/rewrite.ml4 | 67 |
1 files changed, 38 insertions, 29 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 3062ab068..ff617c068 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -552,10 +552,11 @@ let get_rew_rel r = match r.rew_prf with | RewCast c -> mkApp (Coqlib.build_coq_eq (), [| r.rew_car; r.rew_from; r.rew_to |]) let get_rew_prf r = match r.rew_prf with - | RewPrf (rel, prf) -> prf + | RewPrf (rel, prf) -> rel, prf | RewCast c -> - mkCast (mkApp (Coqlib.build_coq_eq_refl (), [| r.rew_car; r.rew_from |]), - c, mkApp (Coqlib.build_coq_eq (), [| r.rew_car; r.rew_from; r.rew_to |])) + let rel = mkApp (Coqlib.build_coq_eq (), [| r.rew_car |]) in + rel, mkCast (mkApp (Coqlib.build_coq_eq_refl (), [| r.rew_car; r.rew_from |]), + c, mkApp (rel, [| r.rew_from; r.rew_to |])) let resolve_subrelation env avoid car rel prf rel' res = if eq_constr rel rel' then res @@ -606,7 +607,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars let evars, proof = proper_proof env evars carrier relation x in [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs' | Some r -> - [ get_rew_prf r; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') + [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') | None -> if y <> None then error "Cannot rewrite the argument of a dependent function"; x :: acc, x :: subst, evars, sigargs, x :: typeargs') @@ -803,7 +804,7 @@ let subterm all flags (s : strategy) : strategy = in match prf with | RewPrf (rel, prf) -> - Some (Some (apply_constraint env avoid res.rew_car rel prf cstr res)) + Some (Some (apply_constraint env avoid res.rew_car rel prf cstr res)) | _ -> Some (Some res) else rewrite_args None @@ -865,35 +866,43 @@ let subterm all flags (s : strategy) : strategy = let cty = Typing.type_of env (goalevars evars) c in let cstr' = Some (mkApp (Lazy.force coq_eq, [| cty |])) in let c' = s env avoid c cty cstr' evars in - (match c' with + let res = + match c' with | Some (Some r) -> let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in Some (Some (coerce env avoid cstr res)) | x -> - if array_for_all ((=) 0) ci.ci_cstr_ndecls then - let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in - let found, brs' = Array.fold_left (fun (found, acc) br -> - if found <> None then (found, fun x -> lift 1 br :: acc x) - else - match s env avoid br ty cstr evars with - | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x) - | _ -> (None, fun x -> lift 1 br :: acc x)) - (None, fun x -> []) brs - in - match found with - | Some r -> - let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in - Some (Some (make_leibniz_proof ctxc ty r)) - | None -> x - else - match try Some (fold_match env (goalevars evars) t) with Not_found -> None with + if array_for_all ((=) 0) ci.ci_cstr_ndecls then + let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in + let found, brs' = Array.fold_left + (fun (found, acc) br -> + if found <> None then (found, fun x -> lift 1 br :: acc x) + else + match s env avoid br ty cstr evars with + | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x) + | _ -> (None, fun x -> lift 1 br :: acc x)) + (None, fun x -> []) brs + in + match found with + | Some r -> + let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in + Some (Some (make_leibniz_proof ctxc ty r)) | None -> x - | Some (cst, _, t') -> - match aux env avoid t' ty cstr evars with - | Some (Some prf) -> Some (Some { prf with - rew_from = t; rew_to = unfold_match env (goalevars evars) cst prf.rew_to }) - | x' -> x) - + else + match try Some (fold_match env (goalevars evars) t) with Not_found -> None with + | None -> x + | Some (cst, _, t') -> + match aux env avoid t' ty cstr evars with + | Some (Some prf) -> + Some (Some { prf with + rew_from = t; rew_to = unfold_match env (goalevars evars) cst prf.rew_to }) + | x' -> x + in + (match res with + | Some (Some r) -> + let rel, prf = get_rew_prf r in + Some (Some (apply_constraint env avoid r.rew_car rel prf cstr r)) + | x -> x) | _ -> None in aux |