From be01deca2b8ff22505adaa66f55f005673bf2d85 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 May 2014 15:06:46 +0200 Subject: More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities). --- test-suite/success/Injection.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 9d5047fdc..6a4882443 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -84,6 +84,38 @@ injection H. intro H0. exact H0. Abort. +(* Test injection using K, knowing that an equality is decidable *) +(* Basic case, using sigT, with "as" clause *) + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + existT P n H1 = existT P n H2 -> H1 = H2. +intros. +injection H as H. +exact H. +Abort. + +(* Test injection using K, knowing that an equality is decidable *) +(* Dependent case not directly exposing sigT *) + +Inductive my_sig (A : Type) (P : A -> Type) : Type := + my_exist : forall x : A, P x -> my_sig A P. + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + my_exist _ _ n H1 = my_exist _ _ n H2 -> H1 = H2. +intros. +injection H as H. +exact H. +Abort. + +(* Test injection using K, knowing that an equality is decidable *) +(* Dependent case not directly exposing sigT deeply nested *) + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + (my_exist _ _ n H1,0) = (my_exist _ _ n H2,0) -> H1 = H2. +intros * [= H]. +exact H. +Abort. + (* Injection does not projects at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. -- cgit v1.2.3