annotate src/system-t.agda @ 1110:45de2b31bf02

add original library and fix for safe mode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 07 Oct 2023 19:43:31 +0900
parents ac53803b3b2a
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
2
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
3 module system-t (U : Set) (V : Set) (v : V) (u : U) where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
4
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Relation.Binary.PropositionalEquality
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 record _×_ ( U : Set ) ( V : Set ) : Set where
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 field
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 π1 : U
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 π2 : V
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
12 <_,_> : {U V : Set} → U → V → U × V
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 < u , v > = record {π1 = u ; π2 = v }
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open _×_
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
18 f : U → V
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
19 f = λ u → v
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 UV : Set
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 UV = U × V
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 uv : U × V
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 uv = < u , v >
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 lemma01 : π1 < u , v > ≡ u
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 lemma01 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 lemma02 : π2 < u , v > ≡ v
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 lemma02 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 lemma03 : (uv : U × V ) → < π1 uv , π2 uv > ≡ uv
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 lemma03 uv = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 lemma04 : (λ x → f x ) u ≡ f u
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 lemma04 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 lemma05 : (λ x → f x ) ≡ f
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 lemma05 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 nn = λ (x : U ) → u
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 n1 = λ ( x : U ) → f x
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 data Bool : Set where
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 T : Bool
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 F : Bool
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
50 D : { U : Set } → U → U → Bool → U
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 D u v T = u
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 D u v F = v
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 data Int : Set where
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 zero : Int
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 S : Int → Int
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
58 pred : Int → Int
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 pred zero = zero
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 pred (S t) = t
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
62 R : { U : Set } → U → ( U → Int → U ) → Int → U
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 R u v zero = u
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 R u v ( S t ) = v (R u v t) t
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
66 null : Int → Bool
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 null zero = T
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 null (S _) = F
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
70 It : { T : Set } → T → (T → T) → Int → T
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 It u v zero = u
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 It u v ( S t ) = v (It u v t )
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
74 R' : { T : Set } → T → ( T → Int → T ) → Int → T
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 R' u v t = π1 ( It ( < u , zero > ) (λ x → < v (π1 x) (π2 x) , S (π2 x) > ) t )
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
77 sum : Int → Int → Int
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
78 sum x y = R y ( λ z → λ w → S z ) x
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
605
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
80 sum2 : Int → Int → Int
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
81 sum2 zero x = x
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
82 sum2 (S x) y = S ( sum2 x y )
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
83
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
84 cong1 : { x y : Int } -> ( f : Int -> Int ) -> x ≡ y -> f x ≡ f y
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
85 cong1 {x} {.x} f refl = refl
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
86
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
87 lemma1 : ( x y : Int ) → sum x y ≡ sum2 x y
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
88 lemma1 zero y = refl
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
89 lemma1 (S x) y = cong1 ( λ z -> S z ) ( lemma1 x y )
af321e38ecee another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 346
diff changeset
90
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
91 mul : Int → Int → Int
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
92 mul x y = R zero ( λ z → λ w → sum y z ) x
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
94 sum' : Int → Int → Int
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
95 sum' x y = R' y ( λ z → λ w → S z ) x
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
97 mul' : Int → Int → Int
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
98 mul' x y = R' zero ( λ z → λ w → sum y z ) x
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
100 fact : Int → Int
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
101 fact n = R (S zero) (λ z → λ w → mul (S w) z ) n
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
103 fact' : Int → Int
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
104 fact' n = R' (S zero) (λ z → λ w → mul (S w) z ) n
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 f3 = fact (S (S (S zero)))
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 f3' = fact' (S (S (S zero)))
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 lemma21 : f3 ≡ f3'
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 lemma21 = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
112 lemma07 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) →
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t )) ≡ t
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 lemma07 u v zero = refl
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
115 lemma07 u v (S t) = cong ( λ x → S x ) ( lemma07 u v t )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
117 lemma06 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → ( (R u v t) ≡ (R' u v t ))
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 lemma06 u v zero = refl
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
119 lemma06 u v (S t) = trans ( cong ( λ x → v x t ) ( lemma06 u v t ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
120 ( cong ( λ y → v (R' u v t) y ) (sym ( lemma07 u v t ) ) )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
122 lemma08 : ( n m : Int ) → ( sum' n m ≡ sum n m )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 lemma08 zero _ = refl
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
124 lemma08 (S t) y = cong ( λ x → S x ) ( lemma08 t y )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
126 lemma09 : ( n m : Int ) → ( mul' n m ≡ mul n m )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 lemma09 zero _ = refl
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
128 lemma09 (S t) y = cong ( λ x → sum y x) ( lemma09 t y )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
130 lemma10 : ( n : Int ) → ( fact n ≡ fact n )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 lemma10 zero = refl
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
132 lemma10 (S t) = cong ( λ x → mul (S t) x ) ( lemma10 t )
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
134 lemma11 : ( n : Int ) → ( fact n ≡ fact' n )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
135 lemma11 n = lemma06 (S zero) (λ z → λ w → mul (S w) z ) n
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
137 lemma06' : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → ( (R u v t) ≡ (R' u v t ))
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 lemma06' u v zero = refl
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 lemma06' u v (S t) = let open ≡-Reasoning in
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 begin
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 R u v (S t)
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 ≡⟨⟩
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 v (R u v t) t
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
144 ≡⟨ cong (λ x → v x t ) ( lemma06' u v t ) ⟩
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 v (R' u v t) t
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
146 ≡⟨ cong (λ x → v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 v (R' u v t) (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t))
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 ≡⟨⟩
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 R' u v (S t)
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
153 sum1 : (x y : Int) → sum x (S y) ≡ S (sum x y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
154 sum1 zero y = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
155 sum1 (S x) y = cong (λ x → S x ) (sum1 x y )
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
156
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
157 sum-sym : (x y : Int) → sum x y ≡ sum y x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
158 sum-sym zero zero = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
159 sum-sym zero (S t) = cong (λ x → S x )( sum-sym zero t)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
160 sum-sym (S t) zero = cong (λ x → S x ) ( sum-sym t zero )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
161 sum-sym (S t) (S t') = let open ≡-Reasoning in
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
162 begin
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
163 sum (S t) (S t')
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
164 ≡⟨⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
165 S (sum t (S t'))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
166 ≡⟨ cong ( λ x → S x ) ( sum1 t t') ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
167 S ( S (sum t t'))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
168 ≡⟨ cong ( λ x → S (S x ) ) ( sum-sym t t') ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
169 S ( S (sum t' t))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
170 ≡⟨ sym ( cong ( λ x → S x ) ( sum1 t' t)) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
171 S (sum t' (S t))
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
172 ≡⟨⟩
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
173 R (S t) ( λ z → λ w → S z ) (S t')
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
174 ≡⟨⟩
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
175 sum (S t') (S t)
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
176
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
177
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
178 sum-assoc : (x y z : Int) → sum x (sum y z ) ≡ sum (sum x y) z
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
179 sum-assoc zero y z = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
180 sum-assoc (S x) y z = let open ≡-Reasoning in
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
181 begin
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
182 sum (S x) ( sum y z )
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
183 ≡⟨⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
184 S ( sum x ( sum y z ) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
185 ≡⟨ cong (λ x → S x ) ( sum-assoc x y z) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
186 S ( sum (sum x y) z )
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
187 ≡⟨⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
188 sum (S ( sum x y)) z
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
189 ≡⟨⟩
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
190 sum (sum (S x) y) z
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
191
315
0d7fa6fc5979 System T and System F
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
193 mul-distr1 : (x y : Int) → mul x (S y) ≡ sum x ( mul x y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
194 mul-distr1 zero y = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
195 mul-distr1 (S x) y = let open ≡-Reasoning in
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
196 begin
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
197 mul (S x) (S y)
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
198 ≡⟨⟩
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
199 sum (S y) (mul x (S y))
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
200 ≡⟨⟩
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
201 S (sum y (mul x (S y) ))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
202 ≡⟨ cong (λ t → S ( sum y t )) (mul-distr1 x y ) ⟩
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
203 S (sum y (sum x (mul x y)))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
204 ≡⟨ cong (λ x → S x ) (
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
205 begin
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
206 sum y (sum x (mul x y))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
207 ≡⟨ sum-assoc y x (mul x y) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
208 sum (sum y x) (mul x y)
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
209 ≡⟨ cong (λ t → sum t (mul x y)) (sum-sym y x ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
210 sum (sum x y) (mul x y)
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
211 ≡⟨ sym ( sum-assoc x y (mul x y)) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
212 sum x (sum y (mul x y))
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
213
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
214 ) ⟩
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
215 S (sum x (sum y (mul x y) ))
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
216 ≡⟨⟩
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
217 S (sum x (mul (S x) y ) )
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
218 ≡⟨⟩
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
219 sum (S x) (mul (S x) y)
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
220
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
221
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
222 mul-sym0 : (x : Int) → mul zero x ≡ mul x zero
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
223 mul-sym0 zero = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
224 mul-sym0 (S x) = mul-sym0 x
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
225
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
226 mul-sym : (x y : Int) → mul x y ≡ mul y x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
227 mul-sym zero x = mul-sym0 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
228 mul-sym (S x) y = let open ≡-Reasoning in
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
229 begin
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
230 mul (S x) y
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
231 ≡⟨⟩
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
232 sum y (mul x y )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
233 ≡⟨ cong ( λ x → sum y x ) (mul-sym x y ) ⟩
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
234 sum y (mul y x)
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
235 ≡⟨ sym ( mul-distr1 y x ) ⟩
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
236 mul y (S x)
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
237
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
238
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
239
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
240 mul-ditr : (y z w : Int) → sum (mul y z) ( mul w z ) ≡ mul (sum y w) z
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
241 mul-ditr y zero w = let open ≡-Reasoning in
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
242 begin
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
243 sum (mul y zero) ( mul w zero )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
244 ≡⟨ cong ( λ t → sum (mul y zero ) t ) (mul-sym w zero ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
245 sum (mul y zero ) ( mul zero w )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
246 ≡⟨ cong ( λ t → sum t zero ) (mul-sym y zero ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
247 sum zero zero
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
248 ≡⟨⟩
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
249 mul zero (sum y w)
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
250 ≡⟨ mul-sym0 (sum y w) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
251 mul (sum y w) zero
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
252
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
253 mul-ditr y (S z) w = let open ≡-Reasoning in
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
254 begin
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
255 sum (mul y (S z)) ( mul w (S z) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
256 ≡⟨ cong ( λ t → sum t ( mul w (S z ))) (mul-distr1 y z) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
257 sum ( sum y ( mul y z)) ( mul w (S z) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
258 ≡⟨ cong ( λ t → sum ( sum y ( mul y z)) t ) (mul-distr1 w z) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
259 sum ( sum y ( mul y z)) ( sum w ( mul w z) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
260 ≡⟨ sym ( sum-assoc y (mul y z ) ( sum w ( mul w z) ) ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
261 sum y ( sum ( mul y z) ( sum w ( mul w z) ))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
262 ≡⟨ cong ( λ t → sum y t) (sum-sym ( mul y z) ( sum w ( mul w z) )) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
263 sum y ( sum ( sum w ( mul w z) )( mul y z))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
264 ≡⟨ sym ( cong ( λ t → sum y t) (sum-assoc w (mul w z) (mul y z )) ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
265 sum y ( sum w (sum ( mul w z) ( mul y z)) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
266 ≡⟨ cong ( λ t → sum y (sum w t) ) ( sum-sym (mul w z) (mul y z )) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
267 sum y ( sum w (sum ( mul y z) ( mul w z)) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
268 ≡⟨ cong ( λ t → sum y (sum w t) ) ( mul-ditr y z w ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
269 sum y ( sum w (mul (sum y w) z) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
270 ≡⟨ sum-assoc y w (mul (sum y w) z) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
271 sum (sum y w) ( mul (sum y w) z )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
272 ≡⟨ sym ( mul-distr1 (sum y w) z ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
273 mul (sum y w) (S z)
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
274
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
275
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
276
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
277 mul-assoc : (x y z : Int) → mul x (mul y z ) ≡ mul (mul x y) z
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
278 mul-assoc zero y z = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
279 mul-assoc (S x) y z = let open ≡-Reasoning in
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
280 begin
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
281 mul (S x) (mul y z )
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
282 ≡⟨⟩
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
283 sum (mul y z) ( mul x ( mul y z ) )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
284 ≡⟨ cong (λ t → sum (mul y z) t ) (mul-assoc x y z ) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
285 sum (mul y z) ( mul ( mul x y) z )
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
286 ≡⟨ mul-ditr y z (mul x y) ⟩
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
287 mul (sum y (mul x y)) z
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
288 ≡⟨⟩
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
289 mul (mul (S x) y) z
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
290
338
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
291
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
292
2f21eb997559 sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
293
339
716f85bc7259 assoc in sysem-T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
294