From c8d96474cfc9af8f5cbb2eb6a3c1da6583a1910a Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 7 Nov 2008 14:18:50 +0000 Subject: Fix a bug in the specialization by unification tactic related to the problems given by injection. Add the example to the test-suite for [dependent destruction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/dependentind.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index d12c21b15..488b057f3 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -102,3 +102,28 @@ Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eapply app with τ... Save. + +(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) + +Unset Manual Implicit Arguments. + +Inductive Ty := + | Nat : Ty + | Prod : Ty -> Ty -> Ty. + +Inductive Exp : Ty -> Type := +| Const : nat -> Exp Nat +| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2) +| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1. + +Inductive Ev : forall t, Exp t -> Exp t -> Prop := +| EvConst : forall n, Ev (Const n) (Const n) +| EvPair : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2', + Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2') +| EvFst : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2, + Ev e (Pair e1 e2) -> + Ev (Fst e) e1. + +Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2). +intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. +Qed. -- cgit v1.2.3