Skip to content

Instantly share code, notes, and snippets.

@SekiT

SekiT/TaPL3.idr

Last active June 6, 2020 09:58
Show Gist options
  • Save SekiT/854d233cbdbc406ad696dcd4417cbcf2 to your computer and use it in GitHub Desktop.
Save SekiT/854d233cbdbc406ad696dcd4417cbcf2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
TaPL3.idr
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