Changes
2 changed files (+39/-6)
-
-
@@ -50,6 +50,34 @@ inductive Term| fls_rec deriving BEq, ReflBEq, LawfulBEq def Term.toString : Term → String | .var x => s!"(list 0n {x})" | .lam b β => s!"(list 1n {toString b} {toString β})" | .app f φ a α => s!"(list 2n {toString f} {toString φ} {toString a} {toString α})" | .typ => "'(3n)" | .new x => s!"(list 4n {x})" | .fn α β => s!"(list 5n {toString α} {toString β})" | .prod α β => s!"(list 6n {toString α} {toString β})" | .and => "'(7n)" | .fst => "'(8n)" | .snd => "'(9n)" | .sum α β => s!"(list 10n {toString α} {toString β})" | .inl => "'(11n)" | .inr => "'(12n)" | .eq a a' α => s!"(list 13n {toString a} {toString a'} {toString α})" | .rfl => "'(14n)" | .eq_rec => "'(15n)" | .nat => "'(16n)" | .zero => "'(17n)" | .succ => "'(18n)" | .nat_rec => "'(19n)" | .fls => "'(20n)" | .fls_rec => "'(21n)" instance : ToString Term := ⟨Term.toString⟩ instance : ToString (Term × Term) := ⟨fun p ↦ s!"(cons {p.1} {p.2})"⟩ -- `infixr` doesn't work at compile time or something notation l " ⇨ " r => Term.fn l r -- \he -- `max` fixes some precedence issues when parsing
-
@@ -230,6 +258,11 @@ def not_not_not_a_imp_not_a := (λ (λ (app ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨#guard check [] not_not_not_a_imp_not_a.1 not_not_not_a_imp_not_a.2 /-- Alternative proof of ¬¬¬A → ¬A -/ def not_not_not_a_imp_not_a' := (λ (λ (app ’1 (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) [λ (app ’0 (₸0 ⇨ ⊥) [’1]) ⊥]) ⊥) (₸0 ⇨ ⊥), (((₸0 ⇨ ⊥) ⇨ ⊥) ⇨ ⊥) ⇨ ₸0 ⇨ ⊥) #guard check [] not_not_not_a_imp_not_a'.1 not_not_not_a_imp_not_a'.2 /-- Convenience wrapper around `.rfl` -/ def rfl' a α := app .rfl (𝒰 ⇨ ’0 ⇨ .eq ’0 ’0 ’1) [α, a]
-
-
-
@@ -349,42 +349,42 @@ def a_imp_a := (Term.lam (.var 0, .new 0), Typ.fn (.new 0) (.new 0))#guard check [] a_imp_a.1 a_imp_a.2 #eval IO.println a_imp_a #eval a_imp_a /-- A → B → B ∧ A -/ def a_imp_b_imp_ba := (Term.lam (.lam (.and (.var 0, .new 1) (.var 1, .new 0), .prod (.new 1) (.new 0)), .fn (.new 1) (.prod (.new 1) (.new 0))), Typ.fn (.new 0) (.fn (.new 1) (.prod (.new 1) (.new 0)))) #guard check [] a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 #eval IO.println a_imp_b_imp_ba #eval a_imp_b_imp_ba /-- A ∧ B → B ∧ A -/ def ab_imp_ba := (Term.lam (.and (.and2 (.var 0, .prod (.new 0) (.new 1)), .new 1) (.and1 (.var 0, .prod (.new 0) (.new 1)), .new 0), .prod (.new 1) (.new 0)), Typ.fn (.prod (.new 0) (.new 1)) (.prod (.new 1) (.new 0))) #guard check [] ab_imp_ba.1 ab_imp_ba.2 #eval IO.println ab_imp_ba #eval ab_imp_ba /-- ¬(A ∨ B) → ¬A -/ def not_ab_imp_not_a := (Term.lam (.lam (.app (.var 1, .fn (.sum (.new 0) (.new 1)) .fls) (.or (.var 0, .new 0), .sum (.new 0) (.new 1)), .fls), .fn (.new 0) .fls), Typ.fn (.fn (.sum (.new 0) (.new 1)) .fls) (.fn (.new 0) .fls)) #guard check [] not_ab_imp_not_a.1 not_ab_imp_not_a.2 #eval IO.println not_ab_imp_not_a #eval not_ab_imp_not_a /-- A → ¬¬A -/ def a_imp_not_not_a := (Term.lam (.lam (.app (.var 0, .fn (.new 0) .fls) (.var 1, .new 0), .fls), .fn (.fn (.new 0) .fls) .fls), Typ.fn (.new 0) (.fn (.fn (.new 0) .fls) .fls)) #guard check [] a_imp_not_not_a.1 a_imp_not_not_a.2 #eval IO.println a_imp_not_not_a #eval a_imp_not_not_a /-- ¬¬¬A → ¬A -/ def not_not_not_a_imp_not_a := (Term.lam (.lam (.app (.var 1, .fn (.fn (.fn (.new 0) .fls) .fls) .fls) (.app a_imp_not_not_a (.var 0, .new 0), .fn (.fn (.new 0) .fls) .fls), .fls), .fn (.new 0) .fls), Typ.fn (.fn (.fn (.fn (.new 0) .fls) .fls) .fls) (.fn (.new 0) .fls)) #guard check [] not_not_not_a_imp_not_a.1 not_not_not_a_imp_not_a.2 #eval IO.println not_not_not_a_imp_not_a #eval not_not_not_a_imp_not_a /-- 2 exists (yeah I know this is not super exciting) -/ def two := (Term.succ ((.succ (.zero, .nat)), .nat), Typ.nat)
-