matching on an inductive with a boolean index

Stream: lean4

[Yuri]

I am a bit confused by why c1 works, but the more intuitive c2 does not:

inductive Bar : Bool → Type where
| val : Nat → Bar false
| add : Bar a → Bar b → Bar (a ∧ b)

def c1 {_ : b == true} : Bar b →  Nat
| .add e1 e2 => 1

def c2 : Bar true → Nat
| .add e1 e2 => 1

[Jovan Gerbscheid]

I think Lean has trouble with the matching when the b in Bar b is something else than a free variable.

Also note that the boolean and function is a && b. Lean accepts a ∧ b because it inserts a coercion from Bool to Prop and from Prop to Bool.

[Aaron Liu]

Lean is having trouble solving the dependent equation decide (a = true ∧ b = true) = true since it doesn't know what e1 and e2 are so this doesn't reduce

[Yuri]

I assumed that .add constructor:

| add : Bar a → Bar b → Bar (a ∧ b)

would give me an automatic proof that a ∧ b = true implies a == true ∧ b == true - after all Lean came to that conclusion by calculating a ∧ b.

btw, I was able to get it to type-check:

def eval(_ : b = false) : Exp b → Nat
| .val x => x
| .add (x : Exp false) (y : Exp false) => eval rfl x + eval rfl y
| .catch (e : Exp false) (h : Exp _)  => eval rfl e
| .catch (e : Exp true) (h : Exp false) =>
  match eval? e with
  | .some n => n
  | .none => eval rfl h

[Aaron Liu]

Yuri said:

I assumed that .add constructor:

| add : Bar a → Bar b → Bar (a ∧ b)

would give me an automatic proof that a ∧ b = true implies a == true ∧ b == true - after all Lean came to that conclusion by calculating a ∧ b.

What do you mean by this? you have a constructor

constructor Bar.add : {a b : Bool} → Bar a → Bar b → Bar (decide (a = true ∧ b = true))

and this is somehow supposed to give you a proof? What do you mean by "calculating" a ∧ b?