Zulip Chat Archive

Stream: new members

Topic: Coq's Program tactic


view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 17:18):

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'

view this post on Zulip Kenny Lau (Dec 16 2018 at 17:27):

-- 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

view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 17:37):

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

view this post on Zulip Kenny Lau (Dec 16 2018 at 17:40):

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

view this post on Zulip Kenny Lau (Dec 16 2018 at 17:40):

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

view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 17:44):

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.

view this post on Zulip Kenny Lau (Dec 16 2018 at 17:46):

right

view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 20:32):

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

view this post on Zulip Chris Hughes (Dec 16 2018 at 20:37):

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

view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 20:42):

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.

view this post on Zulip Chris Hughes (Dec 16 2018 at 20:45):

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

view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 20:54):

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

view this post on Zulip Chris Hughes (Dec 16 2018 at 21:03):

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

view this post on Zulip Wojciech Nawrocki (Dec 16 2018 at 21:21):

Hm that seems to work 🧙, thanks!


Last updated: May 12 2021 at 23:13 UTC