Proof with a subset type · Coq users

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.

I guess at (foo 2 pf), the value of the implicit argument n is automatically figured out by coq.

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".
*)

Julin S (Mar 20 2023 at 20:02):

Looked like the implicit n argument is not being figured out automatically when doing it in proof mode.
Why is that?

Paolo Giarrusso (Mar 20 2023 at 20:08):

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.

Paolo Giarrusso (Mar 20 2023 at 20:14):

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.

Paolo Giarrusso (Mar 20 2023 at 20:15):

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.

Gaëtan Gilbert (Mar 20 2023 at 20:26):

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

Gaëtan Gilbert (Mar 20 2023 at 20:30):

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

Julin S (Mar 24 2023 at 11:46):

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

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

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.

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.

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?

Julin S (Mar 24 2023 at 11:48):

Gaëtan Gilbert (Mar 24 2023 at 11:54):

Gaëtan Gilbert (Mar 24 2023 at 11:56):

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

Stream: Coq users

Topic: Proof with a subset type

Julin S (Mar 20 2023 at 20:00):