diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 58 | ||||
| -rw-r--r-- | tactics/setoid_replace.mli | 3 |
2 files changed, 42 insertions, 19 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 3961ab645..ddeed16d5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -69,27 +69,47 @@ let elimination_sort_of_clause = function | None -> elimination_sort_of_goal | Some id -> elimination_sort_of_hyp id +(* The next function decides in particular whether to try a regular + rewrite or a setoid rewrite. + + Old approach was: + break everything, if [eq] appears in head position + then regular rewrite else try setoid rewrite + + New approach is: + if head position is a known setoid relation then setoid rewrite + else back to the old approach +*) + let general_rewrite_bindings_clause cls lft2rgt (c,l) gl = let ctype = pf_type_of gl c in - let env = pf_env gl in - let sigma = project gl in - let _,t = splay_prod env sigma ctype 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 + (* 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 let general_rewrite_bindings = general_rewrite_bindings_clause None let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings) diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 09fb39da8..b8bed63c5 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -75,3 +75,6 @@ val add_setoid : val new_named_morphism : Names.identifier -> constr_expr -> morphism_signature option -> unit + +val relation_table_find : constr -> relation +val relation_table_mem : constr -> bool |