You can use `False_rect _ _`

in the branch to ask for a proof of `False`

obligation.

Théo Winterhalter said:

You can use

`False_rect _ _`

in the branch to ask for a proof of`False`

obligation.

ah perfect, thanks!

Elaboration is never pretty but it will just be expanded to the corresponding empty match after reduction

```
Compute head.
fun (l : list ?A) (pf : l <> []) =>
match l as c return ((c = [] -> False) -> ?A) with
| [] => fun x : [] = [] -> False =>
match (match x eq_refl return False with end) return ?A with
end
| x :: x0 => ...
```

And you can make a notation like `Notation "!" := (False_rect _ _)`

or someting.

Note that for debug and understand what is going on, you can always use a wildcard to create an obligation and go into proof mode in order to check the context or else

Thank you. So where does the "{ }" notation come from? It is rejected as unknown syntax when I try to reproduce your example.

Well actually in this case, Coq is even smart enough to figure it out on its own

```
Equations? head {A} (l : list A) (pf : l <> nil) : A :=
head [] pf := _;
head (a::l) _ := a.
```

As I was saying it is just the usual with notation,

```
branches of the with
}
```

except that has False has no constructor / branches it is empty

Thomas Lamiaux said:

As I was saying it is just the usual with notation,

`branches of the with }`

except that has False has no constructor / branches it is empty

Ah I didn't get that right, thanks again!

Térence Clastres has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC