hewen.agda

open import Data.Nat         using (ℕ; zero; suc; _+_; _*_; _<′_; _≤′_; _≤_; _<_; _⊔_ )
open import Data.Fin         using (Fin; zero; suc; toℕ; fromℕ;  fromℕ<) renaming (splitAt to FinSplitAt)
open import Data.Maybe as Maybe
open import Relation.Binary.PropositionalEquality
open import Data.Unit        using (⊤; tt)
open import Data.Empty            using (⊥; ⊥-elim)
open import Relation.Nullary      using (¬_; Dec; yes; no)
open import Induction.WellFounded
open import Relation.Binary hiding (_⇒_)
open import Data.Nat.Induction
open import Data.Nat.Properties using  (+-suc; +-comm; ≤-trans; ≤-refl; ≤-reflexive; _≟_; ≤∧≢⇒<; m≤n⇒m<n∨m≡n; _≤?_; m≤m+n; ≤-stepsʳ; ≤-stepsˡ; 1+n≰n )
open import Data.Sum using (_⊎_ )
open import Data.Product          using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_; map)


data Ty :  Set where
  top :  Ty
  _⇒_ : Ty -> Ty -> Ty
  var :  ℕ -> Ty -> Ty 
  ∀<_·_ : Ty -> Ty -> Ty                                                                                     

insert : ℕ -> Ty -> Ty
insert x top = top
insert x (ty ⇒ ty₁) = insert x ty ⇒ insert x ty₁
insert x (var x₁ ty) with x ≤? x₁
... | yes y = var (suc x₁) (insert x ty)
... | no n = var x₁ (insert x ty)
insert x (∀< ty · ty₁) = ∀< insert x ty · insert (suc x) ty₁

weaken : ℕ -> Ty -> Ty
weaken zero x₁ = insert 0 x₁
weaken (suc x) x₁ = insert 0 (weaken x x₁)

update : ℕ -> Ty -> Ty -> Ty
update x u top = top
update x u (t ⇒ t₁) = update x u t ⇒ update x u t₁
update x u (var y t) with x ≟ y
... | yes refl = var y (weaken y u)
... | no n = var y (update x u t)
update x u (∀< t · t₁) = ∀< update x u t · update (suc x) u t₁

push : Ty -> Ty -> Ty
push = update 0

{-
Lemma insert_above_insert : forall (T : typ) (X Y : nat),
  insert (S(X+Y)) (insert X T) = insert X (insert (X+Y) T).
-}


insert_above_insert : ∀{t : Ty} -> ∀{x y : ℕ} -> insert (suc (x + y)) (insert x t) ≡ insert x (insert (x + y) t)
insert_above_insert {top} {x} {y} = refl
insert_above_insert {t ⇒ t₁} {x} {y} rewrite insert_above_insert {t} {x} {y} | insert_above_insert {t₁} {x} {y} = refl
insert_above_insert {var x₁ t} {x} {y} with x ≤? x₁ | x + y ≤? x₁
insert_above_insert {var x₁ t} {x} {y} | yes y1 | yes y2 with  suc (x + y) ≤? suc x₁ |  x ≤? suc x₁
insert_above_insert {var x₁ t} {x} {y} | yes y1 | yes y2 | yes (_≤_.s≤s y3) | yes y4 rewrite insert_above_insert {t} {x} {y} = refl
insert_above_insert {var x₁ t} {x} {y} | yes y1 | yes y2 | yes (_≤_.s≤s y3) | no n4 = ⊥-elim (n4 (≤-trans y1 ( ≤-stepsˡ 1 ≤-refl)))
insert_above_insert {var x₁ t} {x} {y} | yes y1 | yes y2  | no n3 | yes y4 = ⊥-elim (n3 (_≤_.s≤s y2))
insert_above_insert {var x₁ t} {x} {y} | yes y1 | yes y2  | no n3 | no n4 = ⊥-elim (n3 (_≤_.s≤s y2))
insert_above_insert {var x₁ t} {x} {y} | yes y1 | no n2 with suc (x + y) ≤? suc x₁ |  x ≤? x₁
insert_above_insert {var x₁ t} {x} {y} | yes y1 | no n2 | yes (_≤_.s≤s y3) | yes y4 = ⊥-elim (n2 y3)
insert_above_insert {var x₁ t} {x} {y} | yes y1 | no n2 | yes (_≤_.s≤s y3) | no n4 = ⊥-elim (n2 y3) 
insert_above_insert {var x₁ t} {x} {y} | yes y1 | no n2 | no n3 | yes y4 rewrite insert_above_insert {t} {x} {y} = refl
insert_above_insert {var x₁ t} {x} {y} | yes y1 | no n2 | no n3 | no n4 = ⊥-elim (n4 y1)
insert_above_insert {var x₁ t} {x} {y} | no n1 | yes y2 = ⊥-elim (n1 (≤-trans ( ≤-stepsʳ y ≤-refl) y2))
insert_above_insert {var x₁ t} {x} {y} | no n1 | no n2 with suc (x + y) ≤? x₁ | x ≤? x₁
insert_above_insert {var x₁ t} {x} {y} | no n1 | no n2 | yes y3 | yes y4 = ⊥-elim (n1 y4)
insert_above_insert {var x₁ t} {x} {y} | no n1 | no n2 | yes y3 | no n4 = ⊥-elim (n2 (≤-trans (≤-stepsˡ 1 ≤-refl) y3))
insert_above_insert {var x₁ t} {x} {y} | no n1 | no n2 | no n3 | yes y4 =  ⊥-elim (n1 y4)
insert_above_insert {var x₁ t} {x} {y} | no n1 | no n2 | no n3 | no n4 rewrite insert_above_insert {t} {x} {y} = refl
insert_above_insert {∀< t · t₁} {x} {y} rewrite insert_above_insert {t} {x} {y} | insert_above_insert {t₁} {suc x} {y} = refl

{-
Lemma insert_above_weaken : forall (X Y : nat) (T : typ),                                                                                                                                     
   insert (S(X+Y)) (weaken X T) = weaken X (insert Y T).
-}

insert_above_weaken :  ∀{t : Ty} -> ∀{x y : ℕ} -> insert (suc (x + y)) (weaken x t) ≡ weaken x (insert y t)
insert_above_weaken {t} {zero} {y} = insert_above_insert {t} {0} {y} 
insert_above_weaken {t} {suc x} {y} rewrite insert_above_insert {weaken x t} {0} {suc (x + y)} | insert_above_weaken {t} {x} {y} = refl

{-
Lemma insert_above_update : forall (U T : typ) (X Y : nat),                                                                                                                                   
    insert (S(X+Y)) (update X U T)  
  = update X (insert Y U) (insert (S(X+Y)) T).
  -}
  
insert_above_update :  ∀{t u : Ty} -> ∀{x y : ℕ} -> insert (suc (x + y)) (update x u t ) ≡ update x (insert y u) (insert (suc (x + y)) t)
insert_above_update {top} {u} {x} {y} = refl
insert_above_update {t ⇒ t₁} {u} {x} {y} rewrite insert_above_update {t} {u} {x} {y} | insert_above_update {t₁} {u} {x} {y} = refl
insert_above_update {var x₁ t} {u} {x} {y} with  x ≟ x₁ |  suc (x + y) ≤? x₁ 
insert_above_update {var x₁ t} {u} {.x₁} {y} | yes refl | yes y2 = ⊥-elim (1+n≰n  (≤-trans (_≤_.s≤s ( ≤-stepsʳ y ≤-refl)) y2))
insert_above_update {var x₁ t} {u} {.x₁} {y} | yes refl | no n2 with suc (x₁ + y) ≤? x₁ |  x₁ ≟ x₁ 
insert_above_update {var x₁ t} {u} {x₁} {y} | yes refl | no n2 | yes y3 | yes refl = ⊥-elim (n2 y3)
insert_above_update {var x₁ t} {u} {.x₁} {y} | yes refl | no n2 | yes y3 | no n4 = ⊥-elim (n4 refl)
insert_above_update {var x₁ t} {u} {x₁} {y} | yes refl | no n2 | no n3 | yes refl rewrite insert_above_weaken {u} {x₁} {y} = refl
insert_above_update {var x₁ t} {u} {.x₁} {y} | yes refl | no n2 | no n3 | no n4 = ⊥-elim (n4 refl)
insert_above_update {var x₁ t} {u} {x} {y} | no n1 | yes y2 with suc (x + y) ≤? x₁ | x ≟ suc x₁
insert_above_update {var x₁ t} {u} {.(suc x₁)} {y} | no n1 | yes y2 | yes y3 | yes refl = ⊥-elim (1+n≰n (≤-trans (_≤_.s≤s (≤-trans (≤-stepsʳ y ≤-refl) (≤-stepsˡ 1 ≤-refl))) y2))
insert_above_update {var x₁ t} {u} {x} {y} | no n1 | yes y2 | yes y3 | no n4 rewrite insert_above_update {t} {u} {x} {y} = refl
insert_above_update {var x₁ t} {u} {x} {y} | no n1 | yes y2 | no n3 | _ = ⊥-elim (n3 y2)
insert_above_update {var x₁ t} {u} {x} {y} | no n1 | no n2 with suc (x + y) ≤? x₁ | x ≟ x₁
insert_above_update {var x₁ t} {u} {.x₁} {y} | no n1 | no n2 | yes y3 | yes refl = ⊥-elim (n1 refl)
insert_above_update {var x₁ t} {u} {x} {y} | no n1 | no n2 | yes y3 | no n4 = ⊥-elim (n2 y3)
insert_above_update {var x₁ t} {u} {.x₁} {y} | no n1 | no n2 | no n3 | yes refl = ⊥-elim (n1 refl)
insert_above_update {var x₁ t} {u} {x} {y} | no n1 | no n2 | no n3 | no n4 rewrite insert_above_update {t} {u} {x} {y} = refl
insert_above_update {∀< t · t₁} {u} {x} {y} rewrite insert_above_update {t} {u} {x} {y} | insert_above_update {t₁} {u} {suc x} {y} = refl

{-
Lemma insert_on_push : forall (X : nat) (P T : typ),
  insert (S X) (push P T) = push (insert X P) (insert (S X) T).
intros. unfold push. rewrite_for_0 X insert_above_update. reflexivity.
Qed.
-}

insert_on_push :  ∀{t p : Ty} -> ∀{x : ℕ} -> insert (suc x) (push p t) ≡ push (insert x p) (insert (suc x) t)
insert_on_push {t} {p} {x} = insert_above_update {t} {p} {0} {x}

{-
Lemma insert_below_weaken : forall (X Y : nat) (T : typ),                                                                                                                                     
   insert X (weaken (X+Y) T) = weaken (S(X+Y)) T.
-}

insert_below_weaken : ∀{t : Ty} -> ∀{x y : ℕ} -> insert x (weaken (x + y) t) ≡ insert 0 ( weaken (x + y) t )
insert_below_weaken {t} {zero} {y} = refl
insert_below_weaken {t} {suc x} {y} rewrite insert_above_insert {weaken (x + y) t} {0} {x} | insert_below_weaken {t} {x} {y} = refl

{-
Lemma update_above_insert : forall (U T : typ) (X Y : nat),
  update (S(X+Y)) U (insert X T) = insert X (update (X+Y) U T).
-}

jiting : {x y : ℕ} -> x + y ≤ x -> y ≡ 0
jiting {zero} {.zero} _≤_.z≤n = refl
jiting {suc x} {y} (_≤_.s≤s x₁) = jiting x₁

update_above_insert : ∀ {u t : Ty} -> {x y : ℕ} -> update (suc (x + y)) u (insert x t) ≡ insert x (update (x + y) u t)
update_above_insert {u} {top} {x} {y} = refl
update_above_insert {u} {t ⇒ t₁} {x} {y} rewrite update_above_insert {u} {t} {x} {y} | update_above_insert {u} {t₁} {x} {y} = refl
update_above_insert {u} {var x₁ t} {x} {y} with  x ≤? x₁ | x + y ≟ x₁
update_above_insert {u} {var .(x + y) t} {x} {y} | yes y1 | yes refl with suc (x + y) ≟ suc (x + y) | x ≤? x + y
update_above_insert {u} {var .(x + y) t} {x} {y} | yes y1 | yes refl | yes refl | yes y4 rewrite insert_below_weaken {u} {x} {y} = refl
update_above_insert {u} {var .(x + y) t} {x} {y} | yes y1 | yes refl | yes refl | no n4 = ⊥-elim (n4 y1)
update_above_insert {u} {var .(x + y) t} {x} {y} | yes y1 | yes refl | no n3 | _ = ⊥-elim (n3 refl)
update_above_insert {u} {var x₁ t} {x} {y} | yes y1 | no n2 with suc (x + y) ≟ suc x₁ |  x ≤? x₁
update_above_insert {u} {var .(x + y) t} {x} {y} | yes y1 | no n2 | yes refl | yes y4 = ⊥-elim (n2 refl)
update_above_insert {u} {var .(x + y) t} {x} {y} | yes y1 | no n2 | yes refl | no n4 = ⊥-elim (n2 refl)
update_above_insert {u} {var x₁ t} {x} {y} | yes y1 | no n2 | no n3 | yes y4 rewrite update_above_insert {u} {t} {x} {y} = refl
update_above_insert {u} {var x₁ t} {x} {y} | yes y1 | no n2 | no n3 | no n4 = ⊥-elim (n4 y1)
update_above_insert {u} {var .(x + y) t} {x} {y} | no n1 | yes refl = ⊥-elim (n1 (≤-stepsʳ y ≤-refl))
update_above_insert {u} {var x₁ t} {x} {y} | no n1 | no n2 with suc (x + y) ≟ x₁ | x ≤? x₁
update_above_insert {u} {var x₁ t} {x} {y} | no n1 | no n2 | yes y3 | yes y4 = ⊥-elim (n1 y4)
update_above_insert {u} {var .(suc (x + y)) t} {x} {y} | no n1 | no n2 | yes refl | no n4 = ⊥-elim (n4 (≤-trans (≤-stepsʳ y ≤-refl) (≤-stepsˡ 1 ≤-refl)))
update_above_insert {u} {var x₁ t} {x} {y} | no n1 | no n2 | no n3 | yes y4 = ⊥-elim (n1 y4)
update_above_insert {u} {var x₁ t} {x} {y} | no n1 | no n2 | no n3 | no n4 rewrite update_above_insert {u} {t} {x} {y}  = refl
update_above_insert {u} {∀< t · t₁} {x} {y} rewrite update_above_insert {u} {t} {x} {y} | update_above_insert {u} {t₁} {suc x} {y} = refl


{-
Lemma update_above_weaken : forall (X Y : nat) (U T : typ),                                                                                                                                   
  update (S (X + Y)) U (weaken X T) = weaken X (update Y U T).
-}

update_above_weaken :  ∀ {u t : Ty} -> {x y : ℕ} -> update (suc (x + y)) u (weaken x t) ≡ weaken x (update y u t)
update_above_weaken {u} {t} {zero} {y} = update_above_insert {u} {t} {zero} {y}
update_above_weaken {u} {t} {suc x} {y} rewrite update_above_insert {u} {weaken x t} {0} {suc (x + y)} | update_above_weaken {u} {t} {x} {y} = refl

{-
Lemma update_at_insert : forall (U T : typ) (X : nat),
  update X U (insert X T) = insert X T.
-}

update_at_insert :  ∀ {u t : Ty} -> {x : ℕ} -> update x u (insert x t) ≡ insert x t
update_at_insert {u} {top} {x} = refl
update_at_insert {u} {t ⇒ t₁} {x} rewrite update_at_insert {u} {t} {x} | update_at_insert {u} {t₁} {x} = refl
update_at_insert {u} {var x₁ t} {x} with x ≤? x₁
update_at_insert {u} {var x₁ t} {x} | yes y1 with x ≟ suc x₁
update_at_insert {u} {var x₁ t} {.(suc x₁)} | yes y1 | yes refl = ⊥-elim (1+n≰n y1)
update_at_insert {u} {var x₁ t} {x} | yes y1 | no n2 rewrite update_at_insert {u} {t} {x} = refl
update_at_insert {u} {var x₁ t} {x} | no n1 with  x ≟ x₁
update_at_insert {u} {var x₁ t} {.x₁} | no n1 | yes refl = ⊥-elim (n1 ≤-refl)
update_at_insert {u} {var x₁ t} {x} | no n1 | no n2 rewrite update_at_insert {u} {t} {x} = refl
update_at_insert {u} {∀< t · t₁} {x} rewrite update_at_insert {u} {t} {x} | update_at_insert {u} {t₁} {suc x} = refl

{-
Lemma update_below_weaken : forall (U : typ) (X Y : nat) (T : typ),                                                                                                                           
  update X U (weaken (X+Y) T) = weaken (X+Y) T.
-}

update_below_weaken : ∀ {u t : Ty} -> {x y : ℕ} -> update x u (weaken (x + y) t) ≡ weaken (x + y) t 
update_below_weaken {u} {t} {zero} {zero} = update_at_insert {u} {t} {0}
update_below_weaken {u} {t} {zero} {suc y} = update_at_insert {u} {weaken y t} {0} 
update_below_weaken {u} {t} {suc x} {y} rewrite update_above_insert {u} {weaken (x + y) t} {0} {x} | update_below_weaken {u} {t} {x} {y} = refl

{-
Lemma update_at_weaken : forall (X : nat) (T U : typ),                                                                                                                                        
  update X U (weaken X T) = weaken X T.
-}

update_at_weaken : ∀ {u t : Ty} -> {x : ℕ} -> update x u (weaken x t) ≡ weaken x t
update_at_weaken {u} {t} {x} with update_below_weaken {u} {t} {x} {0}
update_at_weaken {u} {t} {x} | z rewrite +-comm x 0 = z

{-
Lemma update_above_update : forall (P U T : typ) (X Y : nat),
    update (S(X+Y)) P (update X U T)
  = update X (update Y P U) (update (S(X+Y)) P T).
-}

update_above_update : ∀ {p u t : Ty} -> {x y : ℕ} -> update (suc (x + y)) p (update x u t) ≡ update x (update y p u) (update (suc (x + y)) p t)
update_above_update {p} {u} {top} {x} {y} = refl
update_above_update {p} {u} {t ⇒ t₁} {x} {y} rewrite update_above_update {p} {u} {t} {x} {y} | update_above_update {p} {u} {t₁} {x} {y} = refl
update_above_update {p} {u} {var x₁ t} {x} {y} with  x ≟ x₁ |  suc (x + y) ≟ x₁
update_above_update {p} {u} {var x₁ t} {.x₁} {y} | yes refl | yes y2 = ⊥-elim (1+n≰n (≤-trans (_≤_.s≤s (≤-stepsʳ y ≤-refl)) (≤-reflexive y2)))
update_above_update {p} {u} {var x₁ t} {.x₁} {y} | yes refl | no n2 with suc (x₁ + y) ≟ x₁ | x₁ ≟ x₁
update_above_update {p} {u} {var x₁ t} {.x₁} {y} | yes refl | no n2 | yes y3 | _ = ⊥-elim (n2 y3)
update_above_update {p} {u} {var x₁ t} {x₁} {y} | yes refl | no n2 | no n3 | yes refl = cong (var x₁) (update_above_weaken {p} {u} {x₁} {y})
update_above_update {p} {u} {var x₁ t} {.x₁} {y} | yes refl | no n2 | no n3 | no n4 = ⊥-elim (n4 refl)
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | yes refl with suc (x + y) ≟ suc (x + y) | x ≟ suc (x + y)
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | yes refl | yes y3 | yes y4 = ⊥-elim (n1 y4)
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | yes refl | yes refl | no n4 with update_below_weaken {update y p u} {p} {x} {1 + y}
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | yes refl | yes refl | no n4 | z rewrite +-comm x (suc y) | +-comm y x = cong (var (suc (x + y))) (sym z)
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | yes refl | no n3 | yes y4 = ⊥-elim (n1 y4)
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | yes refl | no n3 | no n4 = ⊥-elim (n3 refl)
update_above_update {p} {u} {var x₁ t} {x} {y} | no n1 | no n2 with suc (x + y) ≟ x₁  | x ≟ x₁
update_above_update {p} {u} {var x₁ t} {x} {y} | no n1 | no n2 | yes y3 | yes y4 = ⊥-elim (n1 y4)
update_above_update {p} {u} {var .(suc (x + y)) t} {x} {y} | no n1 | no n2 | yes refl | no n4 = ⊥-elim (n2 refl)
update_above_update {p} {u} {var x₁ t} {.x₁} {y} | no n1 | no n2 | no n3 | yes refl = ⊥-elim (n1 refl)
update_above_update {p} {u} {var x₁ t} {x} {y} | no n1 | no n2 | no n3 | no n4 = cong (var x₁) (update_above_update {p} {u} {t} {x} {y})
update_above_update {p} {u} {∀< t · t₁} {x} {y} rewrite update_above_update {p} {u} {t} {x} {y} | update_above_update {p} {u} {t₁} {suc x} {y} = refl

{-
Lemma update_on_push : forall (X : nat) (U P T : typ),                                                                                                         
  update (S X) U (push P T) = push (update X U P) (update (S X) U T).
-}

update_on_push : ∀ {p u t : Ty} -> {x : ℕ} ->  update (suc x) u (push p t) ≡ push (update x u p) (update (suc x) u t) 
update_on_push {p} {u} {t} {x} =  update_above_update {u} {p} {t} {0} {x}

size : Ty -> ℕ
size top = 1
size (x ⇒ x₁) = suc ( size x + size x₁ )
size (var x x₁) = 1
size (∀< x · x₁) = suc ( size x + size x₁ )

insert_preserves_size : ∀ {t : Ty} -> {x : ℕ} -> size (insert x t) ≡ size t
insert_preserves_size {top} {x} = refl
insert_preserves_size {t ⇒ t₁} {x} rewrite insert_preserves_size {t} {x} | insert_preserves_size {t₁} {x} = refl
insert_preserves_size {var x₁ t} {x} with x ≤? x₁
insert_preserves_size {var x₁ t} {x} | yes y1 = refl
insert_preserves_size {var x₁ t} {x} | no n1 = refl
insert_preserves_size {∀< t · t₁} {x} rewrite insert_preserves_size {t} {x} | insert_preserves_size {t₁} {suc x} = refl

weaken_preserves_size : ∀ {t : Ty} -> {x : ℕ} -> size (weaken x t) ≡ size t
weaken_preserves_size {t} {zero} = insert_preserves_size {t} {0}
weaken_preserves_size {t} {suc x} rewrite insert_preserves_size {weaken x t} {0} | weaken_preserves_size {t} {x} = refl

update_preserves_size : ∀ {u t : Ty} -> {x : ℕ} -> size (update x u t) ≡ size t
update_preserves_size {u} {top} {x} = refl
update_preserves_size {u} {t ⇒ t₁} {x} rewrite update_preserves_size {u} {t} {x} | update_preserves_size {u} {t₁} {x} = refl
update_preserves_size {u} {var x₁ t} {x} with  x ≟ x₁
update_preserves_size {u} {var x₁ t} {.x₁} | yes refl = refl
update_preserves_size {u} {var x₁ t} {x} | no n1 = refl
update_preserves_size {u} {∀< t · t₁} {x} rewrite update_preserves_size {u} {t} {x} | update_preserves_size {u} {t₁} {suc x}  = refl

push_preserves_size : ∀ {u t : Ty} -> size (push u t) ≡ size t
push_preserves_size {u} {t} = update_preserves_size {u} {t} {0}

data env : Set where
  [] : env
  _∷_ : Ty -> env -> env
  
postulate
  env_has : env -> ℕ -> Ty -> Set
{-
Inductive wf : env -> typ -> Prop :=                                                                                                                                                      
  | wf_top : forall (E : env),                                           
       wf E top                                                          
  | wf_arrow : forall (E : env) (T1 T2 : typ),                           
       wf E T1 -> wf E T2 -> wf E (arrow T1 T2)                          
  | wf_all : forall (E : env) (T1 T2 : typ),                             
       wf E T1 -> (forall (U : typ), wf (env_push E U) (push U T2)) ->   
       wf E (all T1 T2)                                                  
  | wf_var : forall (E : env) (X : nat) (T1 : typ),                      
       env_has E X T1 -> wf E T1 -> wf E (var X T1). 
-}

data wf : env -> Ty -> Set where
  wf_top : ∀ {E : env} -> wf E top
  wf_arrow : ∀ {E : env} -> {t1 t2 : Ty} -> wf E t1 -> wf E t2 -> wf E (t1 ⇒ t2)
  wf_all : ∀ {E : env} -> {t1 t2 : Ty} -> wf E t1 -> (∀ {u : Ty} -> wf (u ∷ E) (push u t2)) -> wf E (∀< t1 · t2)
  wf_var : ∀ {E : env} -> {x : ℕ} -> {t : Ty} -> env_has E x t -> wf E t -> wf E (var x t)
  

{-
Inductive wf_env : env -> Prop :=                                                                                                                                                             
  | wf_env_empty : wf_env env_empty                                                                                                                            
  | wf_env_push : forall (E : env) (U : typ),                                                                                                                  
       wf_env E -> wf E U -> wf_env (env_push E U).                                                                                                            
-}

data wf_env : env -> Set where
  wf_env_empty : wf_env []
  wf_env_push : ∀{E : env} -> {u : Ty} -> wf_env E -> wf E u -> wf_env ( u ∷ E )

{-
   |                                          -> S <¤ top
   |                                          -> X^U <¤ X^U
   | U <¤ T                                   -> X^U <¤ T
   | T1 <¤ S1 /\ S2 <¤ T2                     -> S1->S2 <¤ T1->T2
   | T1 <¤ S1 /\ (push T1 S2) <¤ (push T1 T2) -> $S1.S2 <¤ $T1.T2
-}

data _<¤_ : Ty -> Ty -> Set where
  unsafe-top : ∀ {t : Ty} -> t <¤ top
  unsafe-refl : ∀ {x : ℕ} -> ∀ {t : Ty} -> var x t <¤ var x t
  unsafe-trans-var : {x : ℕ} -> {u t : Ty} -> u <¤ t ->  var x u <¤ t
  unsafe-arrow : {t1 t2 s1 s2 : Ty} -> t1 <¤ s1 -> s2 <¤ t2  -> ( s1 ⇒ s2 ) <¤ ( t1 ⇒ t2 )
  unsafe-all : {t1 t2 s1 s2 : Ty} ->  t1 <¤ s1 -> (push t1 s2) <¤ (push t1 t2) -> ( ∀< s1 · s2 )  <¤ ( ∀< t1 · t2 )

insert_preserves_sub : {t1 t2 : Ty} -> {x : ℕ} -> t1  <¤ t2 -> (insert x t1)  <¤ (insert x t2)
insert_preserves_sub {t1} {.top} {x} unsafe-top = unsafe-top
insert_preserves_sub {.(var x₁ _)} {.(var x₁ _)} {x} (unsafe-refl {x₁}) with x ≤? x₁
insert_preserves_sub {.(var x₁ _)} {.(var x₁ _)} {x} (unsafe-refl {x₁}) | yes y1 = unsafe-refl
insert_preserves_sub {.(var x₁ _)} {.(var x₁ _)} {x} (unsafe-refl {x₁}) | no n1 = unsafe-refl
insert_preserves_sub {.(var x₂ _)} {t2} {x} (unsafe-trans-var {x₂} x₁) with x ≤? x₂
insert_preserves_sub {.(var x₂ _)} {t2} {x} (unsafe-trans-var {x₂} x₁) | yes y1 = unsafe-trans-var (insert_preserves_sub x₁)
insert_preserves_sub {.(var x₂ _)} {t2} {x} (unsafe-trans-var {x₂} x₁) | no n1 = unsafe-trans-var (insert_preserves_sub x₁)
insert_preserves_sub {.(_ ⇒ _)} {.(_ ⇒ _)} {x} (unsafe-arrow x₁ x₂) = unsafe-arrow (insert_preserves_sub x₁) (insert_preserves_sub x₂)
insert_preserves_sub {.(∀< s1 · s2)} {.(∀< t1 · t2)} {x} (unsafe-all {t1} {t2} {s1 = s1} {s2} x₁ x₂) rewrite sym (insert_on_push {s2} {t1} {x}) = unsafe-all (insert_preserves_sub x₁) lemma where
  lemma :  push (insert x t1) (insert (suc x) s2) <¤  push (insert x t1) (insert (suc x) t2)
  lemma rewrite sym (insert_on_push {s2} {t1} {x}) | sym (insert_on_push {t2} {t1} {x}) = insert_preserves_sub x₂

weaken_preserves_sub : {t1 t2 : Ty} -> {x : ℕ} -> t1  <¤ t2 -> (weaken x t1)  <¤ (weaken x t2)
weaken_preserves_sub {t1} {t2} {zero} x₁ = insert_preserves_sub x₁
weaken_preserves_sub {t1} {t2} {suc x} x₁ = insert_preserves_sub (weaken_preserves_sub {t1} {t2} {x} x₁)

sub-reflexity' : (t : Ty) -> Acc _<_ (size t) -> t <¤ t
sub-reflexity' top x = unsafe-top
sub-reflexity' (t ⇒ t₁) (acc rs) =  unsafe-arrow (sub-reflexity' t (rs _ (_≤_.s≤s ( ≤-stepsʳ (size t₁) ≤-refl))))  (sub-reflexity' t₁ (rs _ (_≤_.s≤s (≤-stepsˡ (size t) ≤-refl))))
sub-reflexity' (var x₁ t) (acc rs) = unsafe-refl
sub-reflexity' (∀< t · t₁) (acc rs) = unsafe-all (sub-reflexity' t (rs _ (_≤_.s≤s ( ≤-stepsʳ (size t₁) ≤-refl)))) (sub-reflexity' (push t t₁) (rs _ (_≤_.s≤s lemma))) where
  lemma : size (update 0 t t₁) ≤ size t + size t₁
  lemma rewrite push_preserves_size {t} {t₁} = ≤-stepsˡ _ ≤-refl

sub-reflexity : (t : Ty) -> t <¤ t
sub-reflexity t = sub-reflexity' t (<-wellFounded (size t))


⇒-eq : ∀{p1 p2 q1 q2 : Ty } -> (p1 ⇒ p2 ) ≡ (q1 ⇒ q2 ) -> ( p1 ≡ q1 ) × ( p2 ≡ q2 )
⇒-eq refl = refl , refl

var-eq : ∀{p q : Ty } -> {a b : ℕ} -> var a p ≡ var b q -> a ≡ b × p ≡ q
var-eq refl = refl , refl

all-eq : ∀{p1 p2 q1 q2 : Ty } -> ∀< p1 · p2 ≡ ∀< q1 · q2 -> p1 ≡ q1 × p2 ≡ q2
all-eq refl = refl , refl

{-
Lemma update_and_equality : forall (P Q T1 T2 : typ) (X : nat),
  update X P T1 = update X P T2 -> update X Q T1 = update X Q T2.
-}

update_and_equality : ∀{p q t1 t2 : Ty} -> {x : ℕ} -> update x p t1 ≡ update x p t2 -> update x q t1 ≡ update x q t2
update_and_equality {p} {q} {top} {top} {x} x₁ = refl
update_and_equality {p} {q} {top} {var x₂ t2} {x} x₁ with  x ≟ x₂
update_and_equality {p} {q} {top} {var x₂ t2} {x₂} () | yes refl
update_and_equality {p} {q} {top} {var x₂ t2} {x} () | no n1
update_and_equality {p} {q} {t1 ⇒ t3} {t2 ⇒ t4} {x} x₁ with ⇒-eq x₁
update_and_equality {p} {q} {t1 ⇒ t3} {t2 ⇒ t4} {x} x₁ | fst , snd  rewrite update_and_equality {p} {q} {t1} {t2} {x} fst | update_and_equality {p} {q} {t3} {t4} {x} snd = refl
update_and_equality {p} {q} {t1 ⇒ t3} {var x₂ t2} {x} x₁ with  x ≟ x₂
update_and_equality {p} {q} {t1 ⇒ t3} {var x₂ t2} {x₂} () | yes refl
update_and_equality {p} {q} {t1 ⇒ t3} {var x₂ t2} {x} () | no n1
update_and_equality {p} {q} {var x₂ t1} {t2} {x} x₁ with  x ≟ x₂
update_and_equality {p} {q} {var x₂ t1} {var x t2} {x₂} x₁ | yes refl with x₂ ≟ x
update_and_equality {p} {q} {var x₂ t1} {var .x₂ t2} {x₂} x₁ | yes refl | yes refl = refl
update_and_equality {p} {q} {var x₂ t1} {var x t2} {x₂} x₁ | yes refl | no n2 with var-eq x₁
update_and_equality {p} {q} {var x₂ t1} {var x t2} {x₂} x₁ | yes refl | no n2 | fst , snd = ⊥-elim (n2 fst)
update_and_equality {p} {q} {var x₂ t1} {var x₃ t2} {x} x₁ | no n1 with  x ≟ x₃
update_and_equality {p} {q} {var x₂ t1} {var x₃ t2} {.x₃} x₁ | no n1 | yes refl with var-eq x₁
update_and_equality {p} {q} {var x₂ t1} {var x₃ t2} {x₃} x₁ | no n1 | yes refl | fst , snd = ⊥-elim (n1 (sym fst))
update_and_equality {p} {q} {var x₂ t1} {var x₃ t2} {x} x₁ | no n1 | no n2 with var-eq x₁
update_and_equality {p} {q} {var .x₃ t1} {var x₃ t2} {x} x₁ | no n1 | no n2 | refl , snd = cong (var x₃) (update_and_equality {p} {q} {t1} {t2} {x} snd)
update_and_equality {p} {q} {∀< t1 · t3} {var x₂ t2} {x} x₁ with x ≟ x₂
update_and_equality {p} {q} {∀< t1 · t3} {var x₂ t2} {x₂} () | yes refl
update_and_equality {p} {q} {∀< t1 · t3} {var x₂ t2} {x} () | no n1
update_and_equality {p} {q} {∀< t1 · t3} {∀< t2 · t4} {x} x₁ with all-eq x₁
update_and_equality {p} {q} {∀< t1 · t3} {∀< t2 · t4} {x} x₁ | fst , snd rewrite update_and_equality {p} {q} {t1} {t2} {x} fst | update_and_equality {p} {q} {t3} {t4} {suc x} snd = refl

hewen : {x : ℕ} -> ∀ {u : Ty} ->  u <¤ var x u -> ⊥
hewen  (unsafe-trans-var x) = {!!}