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`

?

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.

(assuming `l: list nat`

)

Look at `case_eq`

and see how this tactic is implemented by `Print`

ing the obtained term. Then use `refine`

of you want to write code instead of tactics.

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

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

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

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.

Any idea, anyone?

Dominique Larchey-Wendling said:

Look at

`case_eq`

and see how this tactic is implemented by`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.

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

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.

Since `eqn:`

is an option of `destruct`

, you may look at `destruct`

's doc:

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

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

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: Jun 22 2024 at 16:02 UTC