summaryrefslogtreecommitdiff
path: root/test-suite/success/cc.v
blob: fecc89772204d4af15d812dd6c5015c353acf044 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

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.

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.