Quelle unification.txt Sprache: Text

Some notes about the use of unification in Rocq
-----------------------------------------------

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).

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.