Coq's Program tactic

Stream: new members

[Wojciech Nawrocki]

Is there something akin to Coq's Program tactic in Lean? I thought that the equation compiler is basically that, but it seems to fail in the case when it should generate an equality at the type level. In my example:

-- type-level list
inductive InList: list ℕ → ℕ → Type
| Z: ∀ {L n}, InList (n::L) n
| S: ∀ {L n n'}, InList L n → InList (n'::L) n

-- type of functions that map the list L to natural numbers
def ListMap (L) := ∀ {n}, InList L n → ℕ

def id_map {L}: ListMap L := λ n (v: InList L n), n

-- extends m with n
def extend_map {L} (n: ℕ) (m: ListMap L): ListMap (n::L)
:= λ n' (v: InList (n::L) n'),
  match v with
  | InList.Z := sorry -- i would like to synthesize n = n' here
  | InList.S := sorry
  end

the match fails with

type mismatch at application
  _match InList.Z
term
  InList.Z
has type
  InList (?m_1 :: ?m_2) ?m_1
but is expected to have type
  InList (n :: L) n'

[Kenny Lau]

-- type-level list
inductive InList: list ℕ → ℕ → Type
| Z: ∀ {L n}, InList (n::L) n
| S: ∀ {L n n'}, InList L n → InList (n'::L) n

-- type of functions that map the list L to natural numbers
def ListMap (L) := ∀ {n}, InList L n → ℕ

def id_map {L}: ListMap L := λ n (v: InList L n), n

-- extends m with n
def extend_map {L} (n: ℕ) (m: ListMap L): ListMap (n::L)
:= λ n' (v: InList (n::L) n'),
  match n, n', v with
  | n, n', InList.Z := have n = n' := rfl, sorry
  | n, n', InList.S h := sorry
  end

[Wojciech Nawrocki]

Thank you, I was hoping it could be done automatically, but this is fairly concise :)

[Kenny Lau]

no, it is done automatically, have n = n' := rfl is just demonstrating it

[Kenny Lau]

if you put an underscore to replace sorry you will see the lemma being n = n

[Wojciech Nawrocki]

Oh indeed, so it seems the compiler will only equate variables which are being matched rather than everything that v in match v with depends on.

[Kenny Lau]

right

[Wojciech Nawrocki]

Hm no that's not right, it generalizes the matched variable and the state I get in

  match n, n', v with
  | _, _, InList.Z := begin
     -- state here
  end
  | n, n', (InList.S h) := n
  end

is

L : list ℕ,
n : ℕ,
m : ListMap L,
n' : ℕ,
v : InList (n :: L) n',
_match : Π (_a _a_1 : ℕ), InList (_a :: L) _a_1 → ℕ,
_x : ℕ
⊢ ℕ

where n and n' are not equal

[Chris Hughes]

In this state n and n have both effectively been replaced with _x, it just hasn't cleared the old n and n'

[Wojciech Nawrocki]

The example posted here is a bit simplified to make sense without context, but basically I need the n and n' to be equal in the type of v, since my obligation for the return value is that they match, and for that I need the "old" values to be _x so that they can be substituted within v.

[Chris Hughes]

Can you not use InList.Z instead of v. v isn't a variable any more, since you're dealing with the case v = InList.Z

[Wojciech Nawrocki]

Sorry, I oversimplified again. The return type is dependent on n and needs to be a value given as an argument to extend_map. A fuller example:

-- type-level list
inductive InList: list ℕ → ℕ → Type
| Z: ∀ {L n}, InList (n::L) n
| S: ∀ {L n n'}, InList L n → InList (n'::L) n

inductive Foo: ∀ n: ℕ, Type
| A: ∀ n, Foo n
| B: Foo 1
| C: Foo 2

-- type of functions that map the list L to dependent `Foo`s in the list
def ListMap (L) := ∀ {n}, InList L n → Foo n

def id_map {L}: ListMap L := λ n (v: InList L n), Foo.A n

-- extends m with e
def extend_map {L n} (e: Foo n) (m: ListMap L): ListMap (n::L)
:= λ n' (v: InList (n::L) n'),
  match n, n', v with
  | _, _, InList.Z := _ -- needs to be e and have type `Foo n`, but Lean generalizes to type `Foo _x`
  | n, n', (InList.S h) := sorry
  end

[Chris Hughes]

def extend_map {L n} (e: Foo n) (m: ListMap L): ListMap (n::L)
:= λ n' (v: InList (n::L) n'),
  match n, n', v, e with
  | _, _, InList.Z := id -- needs to be e and have type `Foo n`, but Lean generalizes to type `Foo _x`
  | n, n', (InList.S h) := sorry
  end

[Wojciech Nawrocki]

Hm that seems to work 🧙, thanks!