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
|
Implicit Arguments On.
Implicits fst.
Implicits snd.
Module Type PO.
Parameter T:Set.
Parameter le:T->T->Prop.
Axiom le_refl : (x:T)(le x x).
Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z).
Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y).
Hints Resolve le_refl le_trans le_antis.
End PO.
Module Pair[X:PO][Y:PO] <: PO.
Definition T:=X.T*Y.T.
Definition le:=[p1,p2]
(X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
Hints Unfold le.
Lemma le_refl : (p:T)(le p p).
Info Auto.
Qed.
Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
Unfold le; Intuition; Info EAuto.
Qed.
Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
NewDestruct p1.
NewDestruct p2.
Unfold le.
Intuition.
CutRewrite t=t1.
CutRewrite t0=t2.
Reflexivity.
Info Auto.
Info Auto.
Qed.
End Pair.
Read Module Nat.
Module NN := Pair Nat Nat.
Lemma zz_min : (p:NN.T)(NN.le (O,O) p).
Info Auto with arith.
Qed.
|
