From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- dev/doc/unification.txt | 208 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 208 insertions(+) create mode 100644 dev/doc/unification.txt (limited to 'dev/doc/unification.txt') diff --git a/dev/doc/unification.txt b/dev/doc/unification.txt new file mode 100644 index 00000000..6d05bcf5 --- /dev/null +++ b/dev/doc/unification.txt @@ -0,0 +1,208 @@ +Some notes about the use of unification in Coq +---------------------------------------------- + +There are several applications of unification and pattern-matching + +** Unification of types ** + +- For type inference, inference of implicit arguments + * this basically amounts to solve problems of the form T <= U or T = U + where T and U are types coming from a given typing problem + * this kind of problem has to succeed and all the power of unification is + a priori expected (full beta/delta/iota/zeta/nu/mu, pattern-unification, + pruning, imitation/projection heuristics, ...) + +- For lemma application (apply, auto, ...) + * these are also problems of the form T <= U on types but with T + coming from a lemma and U from the goal + * it is not obvious that we always want unification and not matching + * it is not clear which amounts of delta one wants to use + +** Looking for subterms ** + +- For tactics applying on subterms: induction, destruct, rewrite + +- As part of unification of types in the presence of higher-order + evars (e.g. when applying a lemma of conclusion "?P t") + + +---------------------------------------------------------------------- +Here are examples of features one may want or not when looking for subterms + +A- REWRITING + +1- Full conversion on closed terms + +1a- Full conversion on closed terms in the presence of at least one evars (meta) + +Section A1. +Variable y: nat. +Hypothesis H: forall x, x+2 = 0. +Goal y+(1+1) = 0. +rewrite H. +(* 0 = 0 *) +Abort. + +Goal 2+(1+1) = 0. +rewrite H. +(* 0 = 0 *) +Abort. + +(* This exists since the very beginning of Chet's unification for tactics *) +(* But this fails for setoid rewrite *) + +1b- Full conversion on closed terms without any evars in the lemma + +1b.1- Fails on rewrite (because Unification.w_unify_to_subterm_list replaces + unification by check for a syntactic subterm if terms has no evar/meta) + +Goal 0+1 = 0 -> 0+(1+0) = 0. +intros H; rewrite H. +(* fails *) +Abort. + +1b.2- Works with setoid rewrite + +Require Import Setoid. +Goal 0+1 = 0 -> 0+(1+0) = 0. +intros H; rewrite H at 1. +(* 0 = 0 *) +Abort. + +2- Using known instances in full conversion on closed terms + +Section A2. +Hypothesis H: forall x, x+(2+x) = 0. +Goal 1+(1+2) = 0. +rewrite H. +Abort. +End A2. + +(* This exists since 8.2 (HH) *) + +3- Pattern-unification on Rels + +Section A3a. +Variable F: (nat->nat->nat)->nat. +Goal exists f, F (fun x y => f x y) = 0 -> F (fun x y => plus y x) = 0. +eexists. intro H; rewrite H. +(* 0 = 0 *) +Abort. +End A3a. + +(* Works since pattern unification on Meta applied to Rel was introduced *) +(* in unification.ml (8.1, Sep 2006, HH) *) + +Section A3b. +Variables x y: nat. +Variable H: forall f, f x y = 0. +Goal plus y x = 0. +rewrite H. +(* 0 = 0 *) +Abort. +End A3b. + +(* Works since pattern unification on all Meta was supported *) +(* in unification.ml (8.4, Jun 2011, HH) *) + +4- Unification with open terms + +Section A4. +Hypothesis H: forall x, S x = 0. +Goal S 0 = 0. +rewrite (H _). +(* 0 = 0 *) +Abort. +End A4. + +(* Works since unification on Evar was introduced so as to support rewriting *) +(* with open terms (8.2, MS, r11543, Unification.w_unify_to_subterm_list ) *) + +5- Unification of pre-existing evars + +5a- Basic unification of pre-existing evars + +Section A4. +Variables x y: nat. +Goal exists z, S z = 0 -> S (plus y x) = 0. +eexists. intro H; rewrite H. +(* 0 = 0 *) +Abort. +End A4. + +(* This worked in 8.2 and 8.3 as a side-effect of support for rewriting *) +(* with open terms (8.2, MS, r11543) *) + +5b- Pattern-unification of pre-existing evars in rewriting lemma + +Goal exists f, forall x y, f x y = 0 -> plus y x = 0. +eexists. intros x y H; rewrite H. +(* 0 = 0 *) +Abort. + +(* Works since pattern-unification on Evar was introduced *) +(* in unification.ml (8.3, HH, r12229) *) +(* currently governed by a flag: use_evars_pattern_unification *) + +5c- Pattern-unification of pre-existing evars in goal + +Goal exists f, forall x y, plus x y = 0 -> f y x = 0. +eexists. intros x y H; rewrite H. +(* 0 = 0 *) +Abort. + +(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *) + +5d- Mixing pattern-unification of pre-existing evars in goal and evars in lemma + +Goal exists f, forall x, (forall y, plus x y = 0) -> forall y:nat, f y x = 0. +eexists. intros x H y. rewrite H. +(* 0 = 0 *) +Abort. + +(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *) + +6- Multiple non-identical but convertible occurrences + +Tactic rewrite only considers the first one, from left-to-right, e.g.: + +Section A6. +Variable y: nat. +Hypothesis H: forall x, x+2 = 0. +Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)). +rewrite H. +(* 0+(y+(1+1)) = y+(1+1)+0 *) +Abort. +End A6. + +Tactic setoid rewrite first looks for syntactically equal terms and if +not uses the leftmost occurrence modulo delta. + +Require Import Setoid. +Section A6. +Variable y: nat. +Hypothesis H: forall x, x+2 = 0. +Goal (y+(2+0))+(y+2) = (y+2)+(y+(2+0)). +rewrite H at 1 2 3 4. +(* (y+(2+0))+0 = 0+(y+(2+0)) *) +Abort. + +Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)). +rewrite H at 1 2 3 4. +(* 0+(y+(1+1)) = y+(1+1)+0 *) +Abort. +End A6. + +7- Conversion + +Section A6. +Variable y: nat. +Hypothesis H: forall x, S x = 0. +Goal id 1 = 0. +rewrite H. + + +B- ELIMINATION (INDUCTION / CASE ANALYSIS) + +This is simpler because open terms are not allowed and no unification +is involved (8.3). -- cgit v1.2.3