%%%
%%% Author : Brigitte Pientka
%%% Some annotated proofs.
[bp@gs69]$ tutch -v rec.tut
TUTCH 0.51 beta, $Date: 2000/10/27 17:08:48 $
[Opening file rec.tut]
Checking value plus: nat -> nat -> nat
|- fn x => fn y => rec x of p 0 => y | p (s x') => s (p x') end
: nat -> nat -> nat
OK
Proving reflEq: !x:nat. x = x ...
1 [ x: nat;
2 0 = 0; by =NI0
3 [ x': nat, x' = x';
4 s x' = s x' ]; by =NIs 3
5 x = x ]; by NatE 1 2 4
6 !x:nat. x = x by ForallI 5
QED
Proving trans: !x:nat. !y:nat. !z:nat. x = y & y = z => x = z ...
1 [ x: nat;
2 [ y: nat; Case x = 0
3 [ z: nat; Case y = 0
4 [ 0 = 0 & 0 = 0; Case z = 0
5 0 = 0 ]; by =NI0
6 0 = 0 & 0 = 0 => 0 = 0; by ImpI 5
7 [ z': nat, 0 = 0 & 0 = z' => 0 = z'; Case z = s z'
8 [ 0 = 0 & 0 = s z';
9 0 = s z' ]; by AndER 8
10 0 = 0 & 0 = s z' => 0 = s z' ]; by ImpI 9
11 0 = 0 & 0 = z => 0 = z ]; by NatE 3 6 10
12 !z:nat. 0 = 0 & 0 = z => 0 = z; by ForallI 11
13 [ y': nat, !z:nat. 0 = y' & y' = z => 0 = z; Case: y = s y'
14 [ z: nat;
15 [ 0 = s y' & s y' = z;
16 0 = s y'; by AndEL 15
17 0 = z ]; by =NE0s 16
18 0 = s y' & s y' = z => 0 = z ]; by ImpI 17
19 !z:nat. 0 = s y' & s y' = z => 0 = z ]; by ForallI 18
20 !z:nat. 0 = y & y = z => 0 = z ]; by NatE 2 12 19
21 !y:nat. !z:nat. 0 = y & y = z => 0 = z; by ForallI 20
22 [ x': nat, !y:nat. !z:nat. x' = y & y = z => x' = z; Case : x = s x'
23 [ y: nat;
24 [ z: nat;
25 [ s x' = 0 & 0 = z; Case : y = 0
26 s x' = 0; by AndEL 25
27 s x' = z ]; by =NEs0 26
28 s x' = 0 & 0 = z => s x' = z ]; by ImpI 27
29 !z:nat. s x' = 0 & 0 = z => s x' = z; by ForallI 28
30 [ y': nat, !z:nat. s x' = y' & y' = z => s x' = z; Case : y = s y'
31 [ z: nat;
32 [ s x' = s y' & s y' = 0; Case : z = 0
33 s y' = 0; by AndER 32
34 s x' = 0 ]; by =NEs0 33
35 s x' = s y' & s y' = 0 => s x' = 0; by ImpI 34
36 [ z': nat, s x' = s y' & s y' = z' => s x' = z'; Case : z = s z'
37 y' : nat;
38 !z:nat. x' = y' & y' = z => x' = z; by ForallE 22 37
39 z' : nat;
40 x' = y' & y' = z' => x' = z'; by ForallE 38 39
41 [ s x' = s y' & s y' = s z';
42 s x' = s y'; by AndEL 41
43 x' = y'; by =NEss 42
44 s y' = s z'; by AndER 41
45 y' = z'; by =NEss 44
46 x' = y' & y' = z'; by AndI 43 45
47 x' = z'; by ImpE 40 46
48 s x' = s z' ]; by =NIs 47
49 s x' = s y' & s y' = s z' => s x' = s z' ]; by ImpI 48
50 s x' = s y' & s y' = z => s x' = z ]; by NatE 31 35 49
51 !z:nat. s x' = s y' & s y' = z => s x' = z ]; by ForallI 50
52 !z:nat. s x' = y & y = z => s x' = z ]; by NatE 23 29 51
53 !y:nat. !z:nat. s x' = y & y = z => s x' = z ]; by ForallI 52
54 !y:nat. !z:nat. x = y & y = z => x = z ]; by NatE 1 21 53
55 !x:nat. !y:nat. !z:nat. x = y & y = z => x = z by ForallI 54
QED
[Closing file rec.tut]
Proving verPred: !x:nat. ~x = 0 => s (pred x) = x ...
1 [ x: nat;
2 [ ~0 = 0;
3 0 = 0; by =NI0
4 F; by ImpE 2 3
5 s (pred 0) = 0 ]; by FalseE 4
6 ~0 = 0 => s (pred 0) = 0; by ImpI 5
7 [ x': nat, ~x' = 0 => s (pred x') = x';
8 [ ~s x' = 0;
9 !z:nat. z = z; by Lemma refl
10 s x' : nat;
11 s (pred (s x')) = s x' ]; by ForallE 9 10
12 ~s x' = 0 => s (pred (s x')) = s x' ]; by ImpI 11
13 ~x = 0 => s (pred x) = x ]; by NatE 1 6 12
14 !x:nat. ~x = 0 => s (pred x) = x by ForallI 13
QED
[bp@gs69]$