foo.agda

module foo where
open import Relation.Nullary
open import Data.Sum.Base
import Data.String as String
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_;_^_)

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n
  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

data BinTree : Set where
  -- Empty is a tree
  Empty : BinTree
  -- Nodes contain a natural number and two children
  Node : ℕ → BinTree → BinTree → BinTree
  -- Leaves as well
  Leaf : ℕ → BinTree

infix 4 _≤_

sumTree : BinTree → ℕ
sumTree Empty = 0
sumTree (Node n t₀ t₁) = (n + (sumTree t₀)) + (sumTree t₁)
sumTree (Leaf n) = n

data InTree : ℕ → BinTree → Set where
  NodeHere : ∀ n t₀ t₁ → InTree n (Node n t₀ t₁)
  GoLeft   : ∀ n t₀ t₁ → InTree n t₀ → InTree n (Node n t₀ t₁)
  GoRight  : ∀ n t₀ t₁ → InTree n t₁ → InTree n (Node n t₀ t₁)
  LeafHere : ∀ n → InTree n (Leaf n)

n≤n : ∀ n → n ≤ n
n≤n zero = z≤n
n≤n (suc n) = s≤s (n≤n n)

n≤n+_ : ∀ n₀ n₁ → n₀ ≤ n₀ + n₁
(n≤n+ zero) n₁ = z≤n
(n≤n+ (suc n₀)) n₁ = s≤s (n≤n+_ n₀ n₁)

n≤n+_+_ : ∀ n₀ n₁ n₂ → n₀ ≤ n₀ + n₁ + n₂
n≤n+_+_ zero n₁ n₂ = z≤n
n≤n+_+_ (suc n₀) n₁ n₂ = s≤s (n≤n+_+_ n₀ n₁ n₂)

sum≤elem : ∀ (n : ℕ) (t : BinTree) → InTree n t → n ≤ (sumTree t)
sum≤elem n .(Node n t₀ t₁) (NodeHere .n t₀ t₁) = {!!}
sum≤elem n .(Node n t₀ t₁) (GoLeft .n t₀ t₁ n∈t) = {!!}
sum≤elem n .(Node n t₀ t₁) (GoRight .n t₀ t₁ n∈t) = {!!}
sum≤elem n .(Leaf n) (LeafHere .n) = {!!}

data Expr : Set where
  Lit : ℕ → Expr
  Let : String.String → Expr → Expr → Expr
  Plus : Expr → Expr → Expr
  Lam : String.String → Expr → Expr
  App : Expr → Expr → Expr

infixr 4 _×_

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

mutual
  data Value : Set where
    Num : ℕ → Value
    Clo : Expr × Environment → Value
  data Environment : Set where
    Empty : Environment
    Ext : String.String → Value → Environment → Environment

infix 10 _ ⊢ _ ⇓ _



data _⊢_⇓_ : Environment → Expr → Value → Set where
 Const : ∀ {n : ℕ} {Γ : Environment} → Γ ⊢ (Lit n) ⇓ (Num n)