Stream: Coq users

Topic: Proof with a subset type


view this post on Zulip Julin S (Mar 20 2023 at 20:00):

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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 20 2023 at 20:26):

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

view this post on Zulip 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

view this post on Zulip Julin S (Mar 24 2023 at 11:46):

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?

view this post on Zulip Julin S (Mar 24 2023 at 11:48):

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

view this post on Zulip Gaëtan Gilbert (Mar 24 2023 at 11:54):

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

view this post on Zulip Gaëtan Gilbert (Mar 24 2023 at 11:56):

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