I was trying out subset types with something that I copied from the internet.

This is what I tried:

```
Require Import String.
Require Import Lia.
Lemma foo {n:nat} (base:nat): ~(base+n<base).
Proof. lia. Qed.
Definition bar (n:{n:nat|n<2}):string :=
match n with
| exist _ 0 _ => "0"
| exist _ 1 _ => "1"
| exist _ n pf => False_rect string (foo 2 pf )
end.
```

This runs through fine.

I guess at `(foo 2 pf)`

, the value of the implicit argument `n`

is automatically figured out by coq.

But this one gives error:

```
Definition bar' (n:{n:nat|n<2}):string.
refine(
match n with
| exist _ 0 _ => "0"
| exist _ 1 _ => "1"
| exist _ n pf => False_rect string _
end)%string.
Check (foo 2 pf).
(*
In environment
n0 : {n : nat | n < 2}
n : nat
pf : n < 2
n1, n2 : nat
The term "pf" has type "n < 2" while it is expected to have type
"2 + ?n < 2".
*)
```

I guess this got something to do with the way coq works.

What am I missing here?

Looked like the implicit `n`

argument is not being figured out automatically when doing it in proof mode.

Why is that?

To find out more, you can use Set Printing All and print the original bar, with all the annotations filled in; then you'll be able to plug it in step-by-step. To see what refine produced and compare, IIRC you can use Show Proof.

Two things I'll note: (1) if pf had type n < 2 in the first term, I don't see how to infer base such that `foo 2 pf`

typechecks: pf must have type 2 + ?n < 2. It's as if Coq figured that the n bound in the second match must be at least 2. (2) matches carry some type annotations that are inferred. In the first term, inference has strictly more data to work with, since it has the complete term.

I haven't checked how the first declaration works, but I expect the debugging experience to be instructive, and I'm curious what you find out, or to hear extra questions. Please let us know either way.

the match got desugared to something like

```
match n with
exist _ n pf =>
match n return n<2 -> ... with
| 0 | 1 => who cares
| S (S _) as n => fun pf => False_rect ...
end pf
end
```

so in the branch you have `pf : S (S something) < 2`

but this only happens in some of the match compilation strategies (it tries multiple) and since there is no error in the refine case the strategy which produces what you want isn't the one that gets picked

```
Fail Definition bar' (n:{n:nat|n<2}):nat :=
match n with
| exist _ 0 _ => 0
| exist _ 1 _ => 0
| exist _ n pf =>
False_rect nat
ltac:(repeat match goal with
| H := ?v |- _ => idtac H ":=" v; fail
| H : ?t |- _ => idtac H ":" t; fail end;
match goal with |- ?g => idtac "|-" g;
(* the alternate match compilation only gets tried if there's a type error
so don't use fail here*)
exact true
end)
end.
(*
n2 : nat
n1 : nat
pf : (n < 2)
n : nat
n0 : {n : nat | n < 2}
|- False
n := (S (S n2))
n : nat
n2 : nat
n1 : nat
pf : (n3 < 2)
n3 : nat
n0 : {n : nat | n < 2}
|- False
n2 : nat
n1 : nat
pf : (n < 2)
n : nat
n0 : {n : nat | n < 2}
|- False
n := (S (S n2))
n : nat
n2 : nat
n1 : nat
pf : (n3 < 2)
n3 : nat
n0 : {n : nat | n < 2}
|- False
*)
```

you can see `n := S (S n2)`

but not in the first print ie not in the first strategy it tries

Yeah like Gaëtan had said, the terms generated were different.

The one made with `bar`

had the 'more general' `match`

and looked like:

```
Definition bar (n:{n:nat|n<2}):string :=
match n with
| exist _ 0 _ => "0"
| exist _ 1 _ => "1"
| exist _ n pf => False_rect string (foo 2 pf )
end.
Print bar.
(*
bar =
fun n : {n : nat | n < 2} =>
let (n0, pf) := n in
match n0 as n1 return (n1 < 2 -> string) with
| 0 => fun _ : 0 < 2 => "0"%string
| S n1 =>
match n1 as n2 return (S n2 < 2 -> string) with
| 0 => fun _ : 1 < 2 => "1"%string
| S n2 => fun pf0 : S (S n2) < 2 => False_rect string (foo 2 pf0)
end
end pf
: {n : nat | n < 2} -> string
*)
```

And the `bar'`

that I had tried made:

```
Definition bar2 (n:{n:nat|n<2}):string.
refine(
match n with
| exist _ 0 _ => "0"
| exist _ 1 _ => "1"
| exist _ n pf => False_rect string _
end)%string.
Show Proof.
(*
(fun n : {n : nat | n < 2} =>
let (n0, pf) := n in
match n0 with
| 0 => "0"%string
| 1 => "1"%string
| S (S n2 as n1) => False_rect string ?Goal@{n0:=n; n:=n0}
end)
*)
```

So I imitated what I gotten out of `bar`

and did

```
Definition bar' (n:{n:nat|n<2}):string.
refine(
let (n0, pf) := n in
match n0 return n0<2->string with
| 0 => fun _:0<2 => "0"
| S n1 => _
end pf)%string.
refine (
match n1 with
| 0 => _
| S n2 => _
end).
- exact (fun _:1<2 => "1")%string.
- refine (fun pf':S (S n2)<2 => _).
exact (False_rect _ (foo 2 pf')).
Qed.
```

which type checked okay.

The original `bar`

wouldn't work on coq8.6 (tried on an old ubuntu). I guess coq got better at guess-work at a later release.

But I was wondering one thing.

Suppose I wanted to do `bar`

with `{n | n < 10}`

instead of `{n | n < 2}`

.

Does that mean that I would have to make nested matches like that?

Or use a tactic? Is there really no other way for older coq versions?

Oh, I see Gaëtan already gave an ltac command to fix the nested match thing.

that ltac doesn't fix it, it's just for debug printing

instead of `refine`

maybe `destruct`

is nicer

ie

```
Definition bar' (n:{n:nat|n<2}):nat.
Proof.
destruct n as [[|[|n]] H].
1,2:exact 0.
(* last goal has H : S (S n) < 2 *)
```

Last updated: Jun 18 2024 at 08:01 UTC