|
Theorem t1 : forall (A : Set) (a : A) (f : A -> A), f a = a -> f (f a) = a.
intros.
congruence.
Qed.
Theorem t2 :
forall (A : Set) (a b : A) (f : A -> A) (g : A -> A -> A),
a = f a -> g b (f a) = f (f a) -> g a b = f (g b a) -> g a b = a.
intros.
congruence.
Qed.
(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)
Theorem t3 :
forall (N : Set) (o : N) (s d : N -> N),
s (s (s (s (s (s (s (s (s (s (s (s (s (s (s o)))))))))))))) = o ->
s (s (s (s (s (s (s (s (s (s o))))))))) = o ->
s (s (s (s (s (s o))))) = o -> o = s o.
intros.
congruence.
Qed.
(* Examples that fail due to dependencies *)
(* yields transitivity problem *)
Theorem dep :
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x)
(x y : A) (e : x = y) (e0 : f y = g y), f x = g x.
intros; dependent rewrite e; exact e0.
Qed.
(* yields congruence problem *)
Theorem dep2 :
forall (A B : Set)
(f : forall (A : Set) (b : bool), if b then unit else A -> unit)
(e : A = B), f A true = f B true.
intros; rewrite e; reflexivity.
Qed.
(* example that Congruence. can solve
(dependent function applied to the same argument)*)
Theorem dep3 :
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x),
f = g -> forall x : A, f x = g x. intros.
congruence.
Qed.
(* Examples with injection rule *)
Theorem inj1 :
forall (A : Set) (a b c d : A), (a, c) = (b, d) -> a = b /\ c = d.
intros.
split; congruence.
Qed.
Theorem inj2 :
forall (A : Set) (a c d : A) (f : A -> A * A),
f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d.
intros.
congruence.
Qed.
(* Examples with discrimination rule *)
Theorem discr1 : true = false -> False.
intros.
congruence.
Qed.
Theorem discr2 : Some true = Some false -> False.
intros.
congruence.
Qed.
(* example with implications *)
Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D ->
(A -> C) = (B -> D).
congruence.
Qed.
Set Implicit Arguments.
Parameter elt: Set.
Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}.
Definition t (A: Set) := elt -> A.
Definition get (A: Set) (x: elt) (m: t A) := m x.
Definition set (A: Set) (x: elt) (v: A) (m: t A) :=
fun (y: elt) => if elt_eq y x then v else m y.
Lemma gsident:
forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Proof.
intros. unfold get, set. case (elt_eq j i); intro.
congruence.
auto.
Qed.
(* bug 2447 is now closed (PC, 2014) *)
Section bug_2447.
Variable T:Type.
Record R := mkR {x:T;y:T;z:T}.
Variables a a' b b' c c':T.
Lemma bug_2447: mkR a b c = mkR a' b c -> a = a'.
congruence.
Qed.
Lemma bug_2447_variant1: mkR a b c = mkR a b' c -> b = b'.
congruence.
Qed.
Lemma bug_2447_variant2: mkR a b c = mkR a b c' -> c = c'.
congruence.
Qed.
End bug_2447.
(* congruence was supposed to do discriminate but it was bugged for
types with indices *)
Inductive I : nat -> Type := C : I 0 | D : I 0.
Goal ~C=D.
congruence.
Qed.
(* Example by Jonathan Leivant, congruence up to universes *)
Section JLeivant.
Variables S1 S2 : Set.
Definition T1 : Type := S1.
Definition T2 : Type := S2.
Goal T1 = T1.
congruence.
Undo.
unfold T1.
congruence.
Qed.
End JLeivant.
(* An example with primitive projections *)
Module PrimitiveProjections.
Set Primitive Projections.
Record t (A:Type) := { f : A }.
Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0.
congruence.
Undo.
intros.
unfold f in H0. (* internally turn the projection to unfolded form *)
congruence.
Qed.
End PrimitiveProjections.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
