27b7002138
The `checkTargets` function introduced in 4a0f8bf2 as
```
checkTargets (targets : Array Expr) : MetaM Unit := do
let mut foundFVars : FVarIdSet := {}
for target in targets do
unless target.isFVar do
throwError "index in target's type is not a variable (consider using the `cases` tactic instead){indentExpr target}"
if foundFVars.contains target.fvarId! then
throwError "target (or one of its indices) occurs more than once{indentExpr target}"
```
looks like it tries to check for duplicate indices, but it doesn’t
actually, as `foundFVars` is never written to.
This adds
```
foundFVars := foundFVars.insert target.fvarId!
```
and a test case.
Maybe a linter that warns about `let mut` that are never writen to would
be useful?
78 lines
2.2 KiB
Text
78 lines
2.2 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 =>
|
||
trace_state -- `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
|
||
trace_state -- b's type must have been refined, `h` too
|
||
repeat admit
|
||
|
||
inductive Foo : Nat → Nat → Type where
|
||
| mk : Foo 1 2
|
||
|
||
theorem ex4 (n m : Nat) (heq : n = m) (h : Foo n m) : False := by
|
||
induction h using Foo.rec
|
||
case mk => contradiction
|
||
|
||
theorem ex5 (n : Nat) (h : Foo n n) : False := by
|
||
induction h using Foo.rec -- error, target repeated
|