Skip to content

Instantly share code, notes, and snippets.

@jcoglan

jcoglan/proof.txt

Last active May 26, 2017 13:33
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jcoglan/6eb52a5fba45d9a5f67c7ddbaf613dd3 to your computer and use it in GitHub Desktop.
Save jcoglan/6eb52a5fba45d9a5f67c7ddbaf613dd3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
proof.txt
(((λ x : Bool . (λ y : Bool . (x , y))) true) false) . 2
--------------------------------------------------------
----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2
x ← x Bool ← T ∅ ← Γ ∅ ← Γ x ← x Bool ← T ∅ ← Γ x ← x Bool ← T ∅ ← Γ x ← x Bool ← T ∅ ← Γ x ← x Bool ← T
------------------------------------- T-Ctx1 ----- S-x-23 -------- S-T-2 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ----- S-x-24 -------- S-T-2 ------------------------------------- S-Γ-1 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2
(x : Bool) ∈ (∅ , x : Bool) x ← x Bool ← T (∅ , x : Bool) ← Γ y ← x Bool ← T (∅ , x : Bool) ← Γ y ← x Bool ← T y ← x Bool ← T (∅ , x : Bool) ← Γ (∅ , x : Bool) ← Γ y ← x Bool ← T ∅ ← Γ x ← x Bool ← T
----------------------------------------------------------------------------------------------------------------------------------------------- T-Ctx2 ------------------------------------------------------------ S-Γ-1 ----- S-x-23 -------- S-T-2 ----------------------------------------------------------- T-Ctx1 ------------------------------------------------------------ S-Γ-1 ----- S-x-24 -------- S-T-2 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24
(x : Bool) ∈ ((∅ , x : Bool) , y : Bool) ((∅ , x : Bool) , y : Bool) ← Γ x ← x Bool ← T (y : Bool) ∈ ((∅ , x : Bool) , y : Bool) ((∅ , x : Bool) , y : Bool) ← Γ y ← x Bool ← T (∅ , x : Bool) ← Γ y ← x Bool ← T x ← x y ← x x ← x y ← x x ← x y ← x x ← x y ← x x ← x y ← x x ← x y ← x
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Var -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Var ------------------------------------------------------------ S-Γ-1 ----- S-t-0 ----- S-t-0 -------- S-T-2 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-t-0 ----- S-t-0 -------- S-T-2 -------- S-T-2 ----- S-t-0 ----- S-t-0 -------- S-T-2 -------- S-T-2 ----- S-t-0 ----- S-t-0 ----- S-t-0 ----- S-t-0 ----- S-t-0 ----- S-t-0
((∅ , x : Bool) , y : Bool) ⊢ x : Bool ((∅ , x : Bool) , y : Bool) ⊢ y : Bool ((∅ , x : Bool) , y : Bool) ← Γ x ← t y ← t Bool ← T Bool ← T ∅ ← Γ x ← x Bool ← T x ← t y ← t Bool ← T Bool ← T x ← t y ← t Bool ← T Bool ← T x ← t y ← t x ← t y ← t x ← t y ← t
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Pair ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 ------------------------- S-T-1 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 -------- S-T-2 ------------------------- S-T-1 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 -------- S-T-2 -------- S-T-2 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 ----- S-x-24 -------- S-T-2 -------------------- S-t-3
((∅ , x : Bool) , y : Bool) ⊢ (x , y) : (Bool × Bool) (∅ , x : Bool) ← Γ y ← x Bool ← T (x , y) ← t (Bool × Bool) ← T y ← x Bool ← T (x , y) ← t Bool ← T (Bool × Bool) ← T y ← x Bool ← T (x , y) ← t Bool ← T Bool ← T y ← x Bool ← T (x , y) ← t y ← x Bool ← T (x , y) ← t
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Abs ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1 -------------------------------------- S-T-0 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1 -------- S-T-2 ------------------------- S-T-1 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1
(∅ , x : Bool) ⊢ (λ y : Bool . (x , y)) : (Bool → (Bool × Bool)) ∅ ← Γ x ← x Bool ← T (λ y : Bool . (x , y)) ← t (Bool → (Bool × Bool)) ← T ∅ ← Γ x ← x Bool ← T (λ y : Bool . (x , y)) ← t Bool ← T (Bool × Bool) ← T x ← x Bool ← T (λ y : Bool . (x , y)) ← t x ← x Bool ← T (λ y : Bool . (x , y)) ← t
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Abs --------------- T-True ----- S-Γ-0 -------------------------------------------------------------------- S-t-1 -------- S-t-6 -------------------------------------- S-T-0 ----- S-Γ-0 -------------------------------------------------------------------- S-t-1 -------- S-t-6 -------- S-T-2 -------- S-T-2 -------------------------------------------------------------------- S-t-1 -------- S-t-6
∅ ⊢ (λ x : Bool . (λ y : Bool . (x , y))) : (Bool → (Bool → (Bool × Bool))) ∅ ⊢ true : Bool ∅ ← Γ (λ x : Bool . (λ y : Bool . (x , y))) ← t true ← t (Bool → (Bool × Bool)) ← T ∅ ← Γ (λ x : Bool . (λ y : Bool . (x , y))) ← t true ← t Bool ← T Bool ← T (λ x : Bool . (λ y : Bool . (x , y))) ← t true ← t
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-App ---------------- T-False ----- S-Γ-0 ----------------------------------------------------------------------------------------- S-t-2 --------- S-t-7 ------------------------- S-T-1 ----------------------------------------------------------------------------------------- S-t-2 --------- S-t-7
∅ ⊢ ((λ x : Bool . (λ y : Bool . (x , y))) true) : (Bool → (Bool × Bool)) ∅ ⊢ false : Bool ∅ ← Γ ((λ x : Bool . (λ y : Bool . (x , y))) true) ← t false ← t (Bool × Bool) ← T ((λ x : Bool . (λ y : Bool . (x , y))) true) ← t false ← t
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-App ----- S-Γ-0 --------------------------------------------------------------------------------------- S-t-2 -------- S-T-2
∅ ⊢ (((λ x : Bool . (λ y : Bool . (x , y))) true) false) : (Bool × Bool) ∅ ← Γ (((λ x : Bool . (λ y : Bool . (x , y))) true) false) ← t Bool ← T
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Proj2
∅ ⊢ ((((λ x : Bool . (λ y : Bool . (x , y))) true) false) . 2) : Bool
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment