68 lines
1.9 KiB
Text
68 lines
1.9 KiB
Text
inductive Vec (α : Type u) : Nat → Type u
|
||
| nil : Vec α 0
|
||
| cons : α → Vec α n → Vec α (n+1)
|
||
|
||
def Vec.map (xs : Vec α n) (f : α → β) : Vec β n :=
|
||
match xs with
|
||
| nil => nil
|
||
| cons a as => cons (f a) (map as f)
|
||
|
||
def Vec.map' (f : α → β) : Vec α n → Vec β n
|
||
| nil => nil
|
||
| cons a as => cons (f a) (map' f as)
|
||
|
||
def Vec.map2 (f : α → α → β) : Vec α n → Vec α n → Vec β n
|
||
| nil, nil => nil
|
||
| cons a as, cons b bs => cons (f a b) (map2 f as bs)
|
||
|
||
def Vec.head (xs : Vec α (n+1)) : α :=
|
||
match xs with
|
||
| cons x _ => x
|
||
|
||
theorem ex1 (xs ys : Vec α (n+1)) (h : xs = ys) : xs.head = ys.head := by
|
||
induction xs -- error, use cases
|
||
|
||
theorem ex2 (xs ys : Vec α (n+1)) (h : xs = ys) : xs.head = ys.head := by
|
||
cases xs with
|
||
| cons x xs =>
|
||
traceState -- `h` has been refined
|
||
repeat admit
|
||
|
||
inductive ExprType where
|
||
| bool : ExprType
|
||
| nat : ExprType
|
||
|
||
inductive Expr : ExprType → Type
|
||
| natVal : Nat → Expr ExprType.nat
|
||
| boolVal : Bool → Expr ExprType.bool
|
||
| eq : Expr α → Expr α → Expr ExprType.bool
|
||
| add : Expr ExprType.nat → Expr ExprType.nat → Expr ExprType.nat
|
||
|
||
def constProp : Expr α → Expr α
|
||
| Expr.add a b =>
|
||
match constProp a, constProp b with
|
||
| Expr.natVal v, Expr.natVal w => Expr.natVal (v + w)
|
||
| a, b => Expr.add a b
|
||
| e => e
|
||
|
||
abbrev denoteType : ExprType → Type
|
||
| ExprType.bool => Bool
|
||
| ExprType.nat => Nat
|
||
|
||
instance : BEq (denoteType α) where
|
||
beq a b :=
|
||
match α, a, b with
|
||
| ExprType.bool, a, b => a == b
|
||
| ExprType.nat, a, b => a == b
|
||
|
||
def eval : Expr α → denoteType α
|
||
| Expr.natVal v => v
|
||
| Expr.boolVal b => b
|
||
| Expr.eq a b => eval a == eval b
|
||
| Expr.add a b => eval a + eval b
|
||
|
||
theorem ex3 (a b : Expr α) (h : a = b) : eval (constProp a) = eval b := by
|
||
set_option trace.Meta.debug true in
|
||
induction a
|
||
traceState -- b's type must have been refined, `h` too
|
||
repeat admit
|