diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 19:18:06 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 19:18:06 +0000 |
commit | 454ec4db2fcbaef9c67f4b1a4889f47d18795882 (patch) | |
tree | 9dbabcc73533f96d6355643b7fa578341611d658 /test-suite/success/unification.v | |
parent | 6fd6bb20f0263667e23cd02ec03beb8d81b60785 (diff) |
Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed
second-order matching) which was not working correctly in the general
case.
Also made that second-order matching for tactics (abstract_list_all)
uses this algorithm, along the lines of a proposal first experimented
by Dan Grayson (see unification.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/unification.v')
-rw-r--r-- | test-suite/success/unification.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index fdc7c7222..997dceb4d 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -145,3 +145,42 @@ Proof. intros. rewrite H with (f:=f0). Abort. + +(* Three tests provided by Dan Grayson as part of a custom patch he + made for a more powerful "destruct" for handling Voevodsky's + Univalent Foundations. The test checks if second-order matching in + tactic unification is able to guess by itself on which dependent + terms to abstract so that the elimination predicate is well-typed *) + +Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) : + identity (fxe x) (fxe x). +Proof. destruct (fxe x). apply identity_refl. Defined. + +(* a harder example *) + +Definition UU := Type . +Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t. +Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0. +Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1. +Proof. intros t. exact t. Defined. + +Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k). +Proof. + destruct k. + apply idpath. +Defined. + +(* an example with two constructors *) + +Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := +| newfoo1 : foo' x0 x0 +| newfoo2 : foo' x0 x0 . +Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} : + foo' x0 x1 -> foo' x0 x1. +Proof. intros t. exact t. Defined. +Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k). +Proof. + destruct k. + apply idpath. + apply idpath. +Defined. |