Stream: Coq users

Topic: Pattern match on list with a proof

Julin Shaji (Nov 12 2023 at 07:15):

While pattern matching on a list like:

match l with
| [] => _
| x::xs => _
end.

For the x :: xs case, is it possible get also hold on to a proof that l = x::xs?

Julin Shaji (Nov 12 2023 at 07:17):

So that the proof state would look like:

l : list nat
x : nat
xs : list nat
pf: x::xs = l

========================= (1 / 1)

resultType

for the second case.

Julin Shaji (Nov 12 2023 at 07:17):

(assuming l: list nat)

Dominique Larchey-Wendling (Nov 12 2023 at 08:26):

Look at case_eq and see how this tactic is implemented by Printing the obtained term. Then use refine of you want to write code instead of tactics.

Huỳnh Trần Khanh (Nov 12 2023 at 08:39):

there are many times I want this, and every time I realize I don't need it at all

Huỳnh Trần Khanh (Nov 12 2023 at 08:39):

could you provide more context? there's usually a more elegant approach

Pierre Courtieu (Nov 12 2023 at 19:07):

destruct l eqn:heq_l also works (heq_l is the name you give to the equality).
@Huỳnh Trần Khanh It is useless when the destruct is done on a variable because destruct also replace all occurrences of the variable in the goal. But if you destruct on an expression you may really need the hypothesis because the expression may pop up again later in the proof.

Julin Shaji (Nov 13 2023 at 04:51):

Huỳnh Trần Khanh said:

there are many times I want this, and every time I realize I don't need it at all

This is what I had been trying to figure out:

Inductive member {T:Type} (a : T) : list T -> Type :=
| MZ : forall ls, member a (a :: ls)
| MN : forall l ls, member a ls -> member a (l :: ls).

Inductive label {T:Type} (l: list T): Type :=
| Okay: label l
| Label: forall x:T, member x l -> label l.

Definition foo {T:Type} {l:list T} (ls: list (label l)): list (label l).
  refine (
  match l with
  | [] => ls
  | x::l' => _ :: ls
  end).
  refine (Label (x::l') x (MZ x l')).
  (*
  In environment
  T : Type
  l : list T
  ls : list (label l)
  x : T
  l' : list T
  The term "Label (x :: l') x (MZ x l')" has type "label (x :: l')"
  while it is expected to have type "label l".
  *)

I couldn't convince coq that x :: l' is same as l at this point.

Julin Shaji (Nov 13 2023 at 04:53):

Any idea, anyone?

Julin Shaji (Nov 13 2023 at 05:16):

Dominique Larchey-Wendling said:

Look at case_eq and see how this tactic is implemented by Printing the obtained term. Then use refine of you want to write code instead of tactics.

Thanks! Looking at case_eq helped.
There itself they suggest using destruct with eqn: instead.

Julin Shaji (Nov 13 2023 at 05:17):

Pierre Courtieu said:

destruct l eqn:heq_l also works (heq_l is the name you give to the equality).
Huỳnh Trần Khanh It is useless when the destruct is done on a variable because destruct also replace all occurrences of the variable in the goal. But if you destruct on an expression you may really need the hypothesis because the expression may pop up again later in the proof.

Finally got:

Definition foo {T:Type} {l:list T} (ls: list (label l)): list (label l).
  destruct l as [|x l'] eqn:Hcase.
  - exact ls.
  - refine (_ :: ls).
    refine (Label (x::l') x (MZ x l')).
Defined.

Julin Shaji (Nov 13 2023 at 05:18):

I haven't used eqn: before though have seen it a lot in other people's proofs. Which part of docs mention them? Online searching didn't throw many results.

Pierre Castéran (Nov 13 2023 at 07:34):

Since eqn:is an option of destruct, you may look at destruct's doc:

https://coq.inria.fr/doc/V8.18.0/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.destruct

Pierre Courtieu (Nov 13 2023 at 07:41):

In this case though it is better to use case in order to get a simpler term for your function.
To avoid the need for the equality the trick i s to delay introducing ls after destructing on l. like this:

Definition foo {T:Type} {l:list T}:  list (label l) ->  list (label l).
  case l as [|x l']; intros ls.
  - exact nil.
  - refine (_ :: ls).
    refine (Label (x::l') x (MZ x l')).
Defined.

Dominique Larchey-Wendling (Nov 13 2023 at 08:08):

To summarize the different options, favoring lambda terms over proof scripts, you can use either of these:

(** This is the code corresponding to case_eq *)
Definition foo_case_eq {T:Type} {l:list T} (ls : list (label l)) : list (label l).
Proof.
  refine(
  match l as l' return l = l' -> _ with
  | nil => fun e => ls
  | x::l' => fun e => _ :: ls
  end eq_refl).
  rewrite e.
  exact (Label (x::l') x (MZ x l')).
Qed.

(** First variant delaying the introduction of ls *)
Definition foo_delay {T:Type} {l:list T} : list (label l) -> list (label l) :=
  match l with
  | nil => fun ls => ls
  | x::l' => fun ls => Label (x::l') x (MZ x l') :: ls
  end.

(** Second variant using dependent pattern matching *)
Definition foo_dep_pmatch {T:Type} {l:list T} (ls : list (label l)) : list (label l) :=
  match l return list (label l) -> _ with
  | nil => fun ls => ls
  | x::l' => fun ls => Label (x::l') x (MZ x l') :: ls
  end ls.

Lapinot (Nov 13 2023 at 08:53):

I would also add that this is typically a case of dependent pattern matching that Equations helps with handling:

From Equations Require Import Equations.

Equations foo {T} {l:list T} (ls: list (label l)) : list (label l) :=
  foo (l := nil)    ls := ls ;
  foo (l := x :: l) ls := Label (x :: l) x (MZ x l) :: ls .

Last updated: Oct 13 2024 at 01:02 UTC