2
Theorem t1 : forall (A : Set) (a : A) (f : A -> A), f a = a -> f (f a) = a.
8
forall (A : Set) (a b : A) (f : A -> A) (g : A -> A -> A),
9
a = f a -> g b (f a) = f (f a) -> g a b = f (g b a) -> g a b = a.
14
(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)
17
forall (N : Set) (o : N) (s d : N -> N),
18
s (s (s (s (s (s (s (s (s (s (s (s (s (s (s o)))))))))))))) = o ->
19
s (s (s (s (s (s (s (s (s (s o))))))))) = o ->
20
s (s (s (s (s (s o))))) = o -> o = s o.
25
(* Examples that fail due to dependencies *)
27
(* yields transitivity problem *)
30
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x)
31
(x y : A) (e : x = y) (e0 : f y = g y), f x = g x.
32
intros; dependent rewrite e; exact e0.
35
(* yields congruence problem *)
39
(f : forall (A : Set) (b : bool), if b then unit else A -> unit)
40
(e : A = B), f A true = f B true.
41
intros; rewrite e; reflexivity.
45
(* example that Congruence. can solve
46
(dependent function applied to the same argument)*)
49
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x),
50
f = g -> forall x : A, f x = g x. intros.
54
(* Examples with injection rule *)
57
forall (A : Set) (a b c d : A), (a, c) = (b, d) -> a = b /\ c = d.
63
forall (A : Set) (a c d : A) (f : A -> A * A),
64
f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d.
69
(* Examples with discrimination rule *)
71
Theorem discr1 : true = false -> False.
76
Theorem discr2 : Some true = Some false -> False.
81
(* example with implications *)
83
Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D ->
89
Set Implicit Arguments.
92
Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}.
93
Definition t (A: Set) := elt -> A.
94
Definition get (A: Set) (x: elt) (m: t A) := m x.
95
Definition set (A: Set) (x: elt) (v: A) (m: t A) :=
96
fun (y: elt) => if elt_eq y x then v else m y.
98
forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
100
intros. unfold get, set. case (elt_eq j i); intro.
b'\\ No newline at end of file'