Last active
June 6, 2020 09:58
-
-
Save SekiT/854d233cbdbc406ad696dcd4417cbcf2 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Term | |
%default total | |
data Term : Type where | |
Zero : Term | |
True : Term | |
False : Term | |
Succ : Term -> Term | |
Pred : Term -> Term | |
Iszero : Term -> Term | |
If : Term -> Term -> Term -> Term | |
Eq Term where | |
Zero == Zero = True | |
True == True = True | |
False == False = True | |
(Succ t1) == (Succ t1') = t1 == t1' | |
(Pred t1) == (Pred t1') = t1 == t1' | |
(Iszero t1) == (Iszero t1') = t1 == t1' | |
(If t1 t2 t3) == (If t1' t2' t3') = t1 == t1' && t2 == t2' && t3 == t3' | |
_ == _ = False | |
||| Set of constant terms | |
data ConstSet : Type where | |
||| Constructs a set of constants. | |
||| | |
||| Zero, True, False respectively corresponds to the 1st, 2nd, 3rd argument. | |
||| Each argument represents whether the corresponding constant is in the set. | |
Set : Bool -> Bool -> Bool -> ConstSet | |
||| Union of sets | |
union : ConstSet -> ConstSet -> ConstSet | |
union (Set a1 a2 a3) (Set b1 b2 b3) = Set (a1 || b1) (a2 || b2) (a3 || b3) | |
||| Count the number of elements in a set | |
count : ConstSet -> Nat | |
count (Set a1 a2 a3) = (if a1 then 1 else 0) + (if a2 then 1 else 0) + (if a3 then 1 else 0) | |
||| The set of constants in a term | |
consts : Term -> ConstSet | |
consts Zero = Set True False False | |
consts True = Set False True False | |
consts False = Set False False True | |
consts (Succ t1) = consts t1 | |
consts (Pred t1) = consts t1 | |
consts (Iszero t1) = consts t1 | |
consts (If t1 t2 t3) = union (union (consts t1) (consts t2)) (consts t3) | |
||| Depth of a term | |
depth : Term -> Nat | |
depth Zero = 1 | |
depth True = 1 | |
depth False = 1 | |
depth (Succ t1) = (depth t1) + 1 | |
depth (Pred t1) = (depth t1) + 1 | |
depth (Iszero t1) = (depth t1) + 1 | |
depth (If t1 t2 t3) = (max (max (depth t1) (depth t2)) (depth t3)) + 1 | |
||| Size of a term | |
size : Term -> Nat | |
size Zero = 1 | |
size True = 1 | |
size False = 1 | |
size (Succ t1) = (size t1) + 1 | |
size (Pred t1) = (size t1) + 1 | |
size (Iszero t1) = (size t1) + 1 | |
size (If t1 t2 t3) = (size t1) + (size t2) + (size t3) + 1 | |
||| Proof for |union a b| <= |a| + |b| | |
countOfUnion : (a, b : ConstSet) -> LTE (count (union a b)) (count a + count b) | |
countOfUnion (Set False False False) (Set False False False) = lteRefl | |
countOfUnion (Set False False False) (Set False False True ) = lteRefl | |
countOfUnion (Set False False False) (Set False True False) = lteRefl | |
countOfUnion (Set False False False) (Set False True True ) = lteRefl | |
countOfUnion (Set False False False) (Set True False False) = lteRefl | |
countOfUnion (Set False False False) (Set True False True ) = lteRefl | |
countOfUnion (Set False False False) (Set True True False) = lteRefl | |
countOfUnion (Set False False False) (Set True True True ) = lteRefl | |
countOfUnion (Set False False True ) (Set False False False) = lteRefl | |
countOfUnion (Set False False True ) (Set False False True ) = lteSuccRight lteRefl | |
countOfUnion (Set False False True ) (Set False True False) = lteRefl | |
countOfUnion (Set False False True ) (Set False True True ) = lteSuccRight lteRefl | |
countOfUnion (Set False False True ) (Set True False False) = lteRefl | |
countOfUnion (Set False False True ) (Set True False True ) = lteSuccRight lteRefl | |
countOfUnion (Set False False True ) (Set True True False) = lteRefl | |
countOfUnion (Set False False True ) (Set True True True ) = lteSuccRight lteRefl | |
countOfUnion (Set False True False) (Set False False False) = lteRefl | |
countOfUnion (Set False True False) (Set False False True ) = lteRefl | |
countOfUnion (Set False True False) (Set False True False) = lteSuccRight lteRefl | |
countOfUnion (Set False True False) (Set False True True ) = lteSuccRight lteRefl | |
countOfUnion (Set False True False) (Set True False False) = lteRefl | |
countOfUnion (Set False True False) (Set True False True ) = lteRefl | |
countOfUnion (Set False True False) (Set True True False) = lteSuccRight lteRefl | |
countOfUnion (Set False True False) (Set True True True ) = lteSuccRight lteRefl | |
countOfUnion (Set False True True ) (Set False False False) = lteRefl | |
countOfUnion (Set False True True ) (Set False False True ) = lteSuccRight lteRefl | |
countOfUnion (Set False True True ) (Set False True False) = lteSuccRight lteRefl | |
countOfUnion (Set False True True ) (Set False True True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set False True True ) (Set True False False) = lteRefl | |
countOfUnion (Set False True True ) (Set True False True ) = lteSuccRight lteRefl | |
countOfUnion (Set False True True ) (Set True True False) = lteSuccRight lteRefl | |
countOfUnion (Set False True True ) (Set True True True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True False False) (Set False False False) = lteRefl | |
countOfUnion (Set True False False) (Set False False True ) = lteRefl | |
countOfUnion (Set True False False) (Set False True False) = lteRefl | |
countOfUnion (Set True False False) (Set False True True ) = lteRefl | |
countOfUnion (Set True False False) (Set True False False) = lteSuccRight lteRefl | |
countOfUnion (Set True False False) (Set True False True ) = lteSuccRight lteRefl | |
countOfUnion (Set True False False) (Set True True False) = lteSuccRight lteRefl | |
countOfUnion (Set True False False) (Set True True True ) = lteSuccRight lteRefl | |
countOfUnion (Set True False True ) (Set False False False) = lteRefl | |
countOfUnion (Set True False True ) (Set False False True ) = lteSuccRight lteRefl | |
countOfUnion (Set True False True ) (Set False True False) = lteRefl | |
countOfUnion (Set True False True ) (Set False True True ) = lteSuccRight lteRefl | |
countOfUnion (Set True False True ) (Set True False False) = lteSuccRight lteRefl | |
countOfUnion (Set True False True ) (Set True False True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True False True ) (Set True True False) = lteSuccRight lteRefl | |
countOfUnion (Set True False True ) (Set True True True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True True False) (Set False False False) = lteRefl | |
countOfUnion (Set True True False) (Set False False True ) = lteRefl | |
countOfUnion (Set True True False) (Set False True False) = lteSuccRight lteRefl | |
countOfUnion (Set True True False) (Set False True True ) = lteSuccRight lteRefl | |
countOfUnion (Set True True False) (Set True False False) = lteSuccRight lteRefl | |
countOfUnion (Set True True False) (Set True False True ) = lteSuccRight lteRefl | |
countOfUnion (Set True True False) (Set True True False) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True True False) (Set True True True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set False False False) = lteRefl | |
countOfUnion (Set True True True ) (Set False False True ) = lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set False True False) = lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set False True True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set True False False) = lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set True False True ) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set True True False) = lteSuccRight $ lteSuccRight lteRefl | |
countOfUnion (Set True True True ) (Set True True True ) = lteSuccRight $ lteSuccRight $ lteSuccRight lteRefl | |
||| If l <= m, then l + n <= m + n | |
plusNKeepsLTE : (l, m, n : Nat) -> LTE l m -> LTE (l + n) (m + n) | |
plusNKeepsLTE l m Z lt = | |
rewrite plusZeroRightNeutral l in | |
rewrite plusZeroRightNeutral m in lt | |
plusNKeepsLTE l m (S n) lt = | |
rewrite sym $ plusSuccRightSucc l n in | |
rewrite sym $ plusSuccRightSucc m n in | |
LTESucc (plusNKeepsLTE l m n lt) | |
||| If m <= n, then l + m <= l + n | |
nPlusKeepsLTE : (l, m, n : Nat) -> LTE m n -> LTE (l + m) (l + n) | |
nPlusKeepsLTE l m n = | |
rewrite plusCommutative l m in | |
rewrite plusCommutative l n in | |
plusNKeepsLTE m n l | |
||| Proof for Lemma 3.3.3. | |
lemma3_3_3 : (t : Term) -> LTE (count (consts t)) (size t) | |
lemma3_3_3 Zero = LTESucc LTEZero | |
lemma3_3_3 True = LTESucc LTEZero | |
lemma3_3_3 False = LTESucc LTEZero | |
lemma3_3_3 (Succ t1) = lteTransitive (lemma3_3_3 t1) (lteAddRight (size t1)) | |
lemma3_3_3 (Pred t1) = lteTransitive (lemma3_3_3 t1) (lteAddRight (size t1)) | |
lemma3_3_3 (Iszero t1) = lteTransitive (lemma3_3_3 t1) (lteAddRight (size t1)) | |
lemma3_3_3 (If t1 t2 t3) = | |
let c1 = consts t1 in | |
let c2 = consts t2 in | |
let c3 = consts t3 in | |
let l1 = count c1 in | |
let l2 = count c2 in | |
let l3 = count c3 in | |
let s1 = size t1 in | |
let s2 = size t2 in | |
let s3 = size t3 in | |
let lte12_3 = countOfUnion (union c1 c2) c3 in | |
let lte1_2_3 = plusNKeepsLTE (count (union c1 c2)) (l1 + l2) l3 (countOfUnion c1 c2) in | |
let lte123 = lteTransitive lte12_3 lte1_2_3 in | |
let ltes2 = plusNKeepsLTE l1 s1 l2 (lemma3_3_3 t1) in | |
let ltess = nPlusKeepsLTE s1 l2 s2 (lemma3_3_3 t2) in | |
let ltess3 = plusNKeepsLTE (l1 + l2) (s1 + s2) l3 (lteTransitive ltes2 ltess) in | |
let ltesss = nPlusKeepsLTE (s1 + s2) l3 s3 (lemma3_3_3 t3) in | |
rewrite plusCommutative (s1 + s2 + s3) 1 in | |
lteSuccRight (lteTransitive (lteTransitive lte123 ltess3) ltesss) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment