%%% %%% 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]\$