diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 42 |
1 files changed, 37 insertions, 5 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f247f47b6..617bd7717 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -675,10 +675,42 @@ let plain_instance s c = in if s = [] then c else irec c -(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *) -let instance s c = - if s = [] then c else local_strong whd_betaiota (plain_instance s c) - +(* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] + has (unfortunately) different subtle side effects: + + - ** Order of subgoals ** + If the lemma is a case analysis with parameters, it will move the + parameters as first subgoals (e.g. "case H" applied on + "H:D->A/\B|-C" will present the subgoal |-D first while w/o + betaiota the subgoal |-D would have come last). + + - ** Betaiota-contraction in statement ** + If the lemma has a parameter which is a function and this + function is applied in the lemma, then the _strong_ betaiota will + contract the application of the function to its argument (e.g. + "apply (H (fun x => x))" in "H:forall f, f 0 = 0 |- 0=0" will + result in applying the lemma 0=0 in which "(fun x => x) 0" has + been contracted). A goal to rewrite may then fail or succeed + differently. + + - ** Naming of hypotheses ** + If a lemma is a function of the form "fun H:(forall a:A, P a) + => .. F H .." where the expected type of H is "forall b:A, P b", + then, without reduction, the application of the lemma will + generate a subgoal "forall a:A, P a" (and intro will use name + "a"), while with reduction, it will generate a subgoal "forall + b:A, P b" (and intro will use name "b"). + + - ** First-order pattern-matching ** + If a lemma has the type "(fun x => p) t" then rewriting t may fail + if the type of the lemma is first beta-reduced (this typically happens + when rewriting a single variable and the type of the lemma is obtained + by meta_instance (with empty map) which itself call instance with this + empty map. + *) + +let instance s c = + (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -876,7 +908,7 @@ let meta_instance env b = List.map (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) in - instance c_sigma b.rebus + if c_sigma = [] then b.rebus else instance c_sigma b.rebus let nf_meta env c = meta_instance env (mk_freelisted c) |