|
Require Eqdep_dec.
(* Check the behaviour of Injection *)
(* Check that Injection tries Intro until *)
Unset Structural Injection.
Lemma l1 : forall x : nat, S x = S (S x) -> False.
injection 1.
apply n_Sn.
Qed.
Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False.
injection H.
intros.
apply (n_Sn x H0).
Qed.
(* Check that no tuple needs to be built *)
Lemma l3 :
forall x y : nat,
existT (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
existT (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
x = y.
intros x y H.
injection H.
exact (fun H => H).
Qed.
(* Check that a tuple is built (actually the same as the initial one) *)
Lemma l4 :
forall p1 p2 : {0 = 0} + {0 = 0},
existT (fun n : nat => {n = n} + {n = n}) 0 p1 =
existT (fun n : nat => {n = n} + {n = n}) 0 p2 ->
existT (fun n : nat => {n = n} + {n = n}) 0 p1 =
existT (fun n : nat => {n = n} + {n = n}) 0 p2.
intros.
injection H.
exact (fun H => H).
Qed.
Set Structural Injection.
(* Test injection as *)
Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z.
intros; injection H as Hxz Hyt.
exact Hxz.
Qed.
(* Check the variants of injection *)
Goal forall x y, S x = S y -> True.
injection 1 as H'.
Undo.
intros.
injection H as H'.
Undo.
Ltac f x := injection x.
f H.
Abort.
Goal (forall x y : nat, x = y -> S x = S y) -> True.
intros.
try injection (H O) || exact I.
Qed.
Goal (forall x y : nat, x = y -> S x = S y) -> True.
intros.
einjection (H O).
2:instantiate (1:=O).
Abort.
Goal (forall x y : nat, x = y -> S x = S y) -> True.
intros.
einjection (H O ?[y]) as H0.
instantiate (y:=O).
Abort.
(* Test the injection intropattern *)
Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b.
intros * [= H1 H2].
exact H1.
Qed.
(* Test injection using K, knowing that an equality is decidable *)
(* Basic case, using sigT *)
Scheme Equality for nat.
Unset Structural Injection.
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.
intro H0. exact H0.
Abort.
Set Structural Injection.
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 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.
(* Test the Keep Proof Equalities option. *)
Set Keep Proof Equalities.
Unset Structural Injection.
Inductive pbool : Prop := Pbool1 | Pbool2.
Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell.
Goal Pbsc Pbool1 = Pbsc Pbool2 -> True.
injection 1.
match goal with
|- Pbool1 = Pbool2 -> True => idtac | |- True => fail
end.
Abort.
(* Injection in the presence of local definitions *)
Inductive A := B (T := unit) (x y : bool) (z := x).
Goal forall x y x' y', B x y = B x' y' -> y = y'.
intros * [= H1 H2].
exact H2.
Qed.
(* Injection does not project at positions in Prop... allow it?
Inductive t (A:Prop) : Set := c : A -> t A.
Goal forall p q : True\/True, c _ p = c _ q -> False.
intros.
injection H.
Abort.
*)
(* Injection does not project on discriminable positions... allow it?
Goal 1=2 -> 1=0.
intro H.
injection H.
intro; assumption.
Qed.
*)
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
