Stream: Coq users

Topic: Proving properties of programs using the Specif sig type


view this post on Zulip Radosław Waśko (May 12 2021 at 11:09):

Hello, I hope this is the right place to ask this question.
I'm working on a project where we are creating operations using subset types, i.e. { x : T | P x } and I have trouble proving properties of functions that return values but also need the proofs - I'm not sure how to describe this well so let me just paste a simple example:

Require Import BinInt.

Open Scope Z.

Definition Foo := { x : Z | x < 100 }.

Definition embed (x : Z) : option Foo.
  destruct (Z.ltb x 100) as []eqn:Hg.
  - apply Some.
    eapply exist with x.
    apply Z.ltb_lt in Hg.
    assumption.
  - apply None.
Defined.

Definition val (x : Foo) : Z := proj1_sig x.

We define a datatype Foo which is integers < 100 and I'm creating a function embed which takes an integer, and if it is < 100, returns Foo (wrapped in Some) and otherwise returns None.
Now I want to prove that the embedding is 'full' that is, for every integer that fits, it returns a valid value:

Lemma embed_full : forall x,
    x < 100 ->
    exists r, embed x = Some r /\ val r = x.

And here is where I get stuck. How can I try proving this?
I have tried the following strategy - unfold the definition, use the assumption to decide the <? inequality and rewrite it in the definition to be able to partially evaluate the embed function:

  intros.
  unfold embed.
  assert (HR: x <? 100 = true).
  - apply Z.ltb_lt. assumption.
  - rewrite HR.

However on the last operation (rewrite), I get the following error:

Error: Abstracting over the term "x <? 100" leads to a term
fun b : bool =>
exists r : Foo,
  (if b as b0 return (b = b0 -> option Foo)
   then
    fun Hg : b = true =>
    Some
      (exist (fun x0 : Z => x0 < 100) x
         (match Z.ltb_lt x 100 with
          | conj H0 _ => H0
          end Hg))
   else fun _ : b = false => None) eq_refl = Some r /\ val r = x
which is ill-typed.
Reason is: Incorrect elimination of "Z.ltb_lt x 100" in the inductive type "and":
ill-formed elimination predicate.

view this post on Zulip Radosław Waśko (May 12 2021 at 11:11):

It seems to me that the issue is that I'm doing this destruct with equations, which creates the if which is abstracted over the equation.
However, I don't know how to define embed in a different way, because that is precisely what it needs to be doing - it needs to check the <? comparison and it needs the additional information about the result to deduce the proof for the { _ | x < 100 } property.

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 12:33):

I'm not sure about your specific issue, but I would define embed differently, and then the problem becomes easy:

Require Import BinInt.
Open Scope Z.

Definition Foo := { x : Z | x < 100 }.

Axiom lt100_dec : forall x : Z, {x < 100} + {~ (x < 100)}.

Definition embed (x : Z) : option Foo :=
  match lt100_dec x with
  | left ltx100 => Some (exist _ x ltx100)
  | right _ => None
  end.

Definition val (x : Foo) : Z := proj1_sig x.

Lemma embed_full : forall x,
    x < 100 ->
    exists r, embed x = Some r /\ val r = x.
Proof.
  intros x ltx100.
  unfold embed.
  destruct (lt100_dec x); [| contradiction].
  exists (exist _ x l).
  split; reflexivity.
Qed.

(There must be some lemma that subsumes lt100_dec, I just couldn't find it in a couple of seconds.)

view this post on Zulip Radosław Waśko (May 12 2021 at 12:37):

Ana de Almeida Borges said:

I'm not sure about your specific issue, but I would define embed differently, and then the problem becomes easy:

Require Import BinInt.
Open Scope Z.

Definition Foo := { x : Z | x < 100 }.

Axiom lt100_dec : forall x : Z, {x < 100} + {~ (x < 100)}.

Definition embed (x : Z) : option Foo :=
  match lt100_dec x with
  | left ltx100 => Some (exist _ x ltx100)
  | right _ => None
  end.

Definition val (x : Foo) : Z := proj1_sig x.

Lemma embed_full : forall x,
    x < 100 ->
    exists r, embed x = Some r /\ val r = x.
Proof.
  intros x ltx100.
  unfold embed.
  destruct (lt100_dec x); [| contradiction].
  exists (exist _ x l).
  split; reflexivity.
Qed.

(There must be some lemma that subsumes lt100_dec, I just couldn't find it in a couple of seconds.)

Awesome! That seems to be exactly what I needed.

view this post on Zulip Meven Lennon-Bertrand (May 12 2021 at 12:38):

A solution similar to the one above, using a reflection lemma from the library :

Require Import BinInt.

Open Scope Z.

Definition Foo := { x : Z | x < 100 }.

Definition embed (x : Z) : option Foo.
Proof.
  destruct (Z.ltb_spec0 x 100).
  - apply Some.
    exists x.
    assumption.
  - exact None.
Defined.

Definition val (x : Foo) : Z := proj1_sig x.

Lemma embed_full : forall x,
    x < 100 ->
    exists r, embed x = Some r /\ val r = x.
Proof.
  intros.
  unfold embed.
  destruct (Z.ltb_spec0 x 100).
  - now exists (exist _ x l).
  - now exfalso.
Qed.

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 12:38):

In general if you need to use a proof during a definition you can match on {thing holds} + {thing doesn't hold} (assuming it's decidable) and use the proofs stored in the {_} + {_} datatype (called sumbool)

view this post on Zulip Meven Lennon-Bertrand (May 12 2021 at 12:40):

The other possibility (and the one pushed especially by the MathComp library) is to use the Bool.reflect inductive to achieve a goal somewhat similar to what one would obtain using sumbool, ie. working with decidable predicates.

view this post on Zulip Radosław Waśko (May 12 2021 at 12:42):

Thanks a lot for the answers!
I think I will try going with the sumbool type as it seems it should be quite easy to handle with extraction to OCaml later on (I assume as the proofs are erased, these functions will become isomorphic with functions returning booleans).

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 12:44):

I assume as the proofs are erased, these functions will become isomorphic with functions returning booleans

Yup.

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 12:46):

It's typical to include the following line before extraction to take advantage of this:

Extract Inductive sumbool => "bool" [ "true" "false" ].

i.e., left is mapped to true and right to false

view this post on Zulip Meven Lennon-Bertrand (May 12 2021 at 12:46):

Now I’m wondering what reflect is erased to!

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 12:53):

Something isomorphic:

Require Import Bool Extraction.
Extraction reflect.
(*
type reflect =
| ReflectT
| ReflectF
*)

view this post on Zulip Michael Soegtrop (May 12 2021 at 13:14):

IMHO the solution of @Ana de Almeida Borges with a definition in plain gallina is preferable over the solution of @Meven Lennon-Bertrand . One should avoid to use tactics to create computational definitions, because they might be hard to work with and the exact term might even change with Coq versions, so that your proofs about it break. I would use tactics only, if the actual term is not interesting - as in the case of proofs. In my experience you spend 100x of what you save in time to write your definition with tactics later in proofs - what you witnessed is only the tip of the ice berg.

What I sometimes do if I can't figure it out is to use tactics to create a definition, then print the proof term and learn from it.

When you write functions which shall compute, it does make sense to try something like Eval cbv in embed 20.. You will see that both solutions, the one from Ana and the one from Meven will lead to a term blow up with the size of the 100. If you do the same with 2^32 instead of 100, the cbv will fail. Have a look at this:

Require Import ZArith.
Open Scope Z.

Definition Foo := { x : Z | x < 100 }.

Definition embed (x : Z) : option Foo :=
  match Z_lt_le_dec x 100 with
  | left ltx100 => Some (exist _ x ltx100)
  | right _ => None
  end.

Eval cbv in embed 20.

which results in

     = Some
         (exist
            (fun x : Z =>
             match x with
             | 100 => Eq
             | 0 | 95 | 63 | 79 | 47 | 31 | 87 | 55 | 71 | 39 |
               23 | 15 | 91 | 59 | 75 | 43 | 27 | 83 | 51 | 99 |
               67 | 35 | 19 | 11 | 7 | 93 | 61 | 77 | 45 | 29 |
               85 | 53 | 69 | 37 | 21 | 13 | 89 | 57 | 73 | 41 |
               25 | 81 | 49 | 97 | 65 | 33 | 17 | 9 | 5 | 3 |
               94 | 62 | 78 | 46 | 30 | 86 | 54 | 70 | 38 | 22 |
               14 | 90 | 58 | 74 | 42 | 26 | 82 | 50 | 98 | 66 |
               34 | 18 | 10 | 6 | 92 | 60 | 76 | 44 | 28 | 84 |
               52 | 68 | 36 | 20 | 12 | 88 | 56 | 72 | 40 | 24 |
               80 | 48 | 96 | 64 | 32 | 16 | 8 | 4 | 2 | 1 | Z.neg _ => Lt
             | _ => Gt
             end = Lt) 20 eq_refl)
     : option Foo

If you swap the relational operator, magically you get a term which does not increase with the upper limite:

Require Import ZArith.
Open Scope Z.

Definition Foo := { x : Z | 10000 > x}.

Definition embed (x : Z) : option Foo :=
  match Z_gt_le_dec 10000 x with
  | left P => Some (exist _ x P)
  | right _ => None
  end.

Eval cbv in embed 20.

gives

     = Some
         (exist
            (fun y : Z =>
             match y with
             | Z.pos y' =>
                 (fix compare_cont (r : comparison) (x y0 : positive) {struct y0} :
                      comparison :=
                    match x with
                    | (p~1)%positive =>
                        match y0 with
                        | (q~1)%positive => compare_cont r p q
                        | (q~0)%positive => compare_cont Gt p q
                        | 1%positive => Gt
                        end
                    | (p~0)%positive =>
                        match y0 with
                        | (q~1)%positive => compare_cont Lt p q
                        | (q~0)%positive => compare_cont r p q
                        | 1%positive => Gt
                        end
                    | 1%positive => match y0 with
                                    | 1%positive => r
                                    | _ => Lt
                                    end
                    end) Eq 10000%positive y'
             | _ => Gt
             end = Gt) 20 eq_refl)
     : option Foo

The Z Prop relational operators are well known to be brittle in such situations, because they are computational. You must take care that constants are abstracted or not the one one which the definition recurses.

view this post on Zulip Michael Soegtrop (May 12 2021 at 13:24):

P.S.: the interesting point is that the computations even blows up with a ground term like embed 20.

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 13:31):

If you swap the relational operator, magically you get a term which does not increase with the upper limite:

Interesting! But why? Or rather, is there a way to find out without trying both?

view this post on Zulip Ana de Almeida Borges (May 12 2021 at 13:33):

Oh, is it because compare is defined decreasing on the second argument?

view this post on Zulip Meven Lennon-Bertrand (May 12 2021 at 13:39):

Thanks for the detailed infos!
On a side-note though, I would say using tactics to construct terms as I do is not that harmful if you use tactics like case, exists, assumption and the like that behave mostly like refine with some term former (exists or split are inductive constructors, assumption a variable, case a match, intros lambda-abstractions…). But I agree that in general tactics can be quite dangerous.

view this post on Zulip Michael Soegtrop (May 12 2021 at 14:18):

Ana de Almeida Borges said:

Oh, is it because compare is defined decreasing on the second argument?

yes, exactly. This kind of thing regularly happens if a term contains variables, but it gets problematic when it happens with ground terms like embed 20, because this means one never can't compute anything if numbers get large. Also note, that vm_compute and cbv might lead to different results here, so one should verify that both work.

view this post on Zulip Michael Soegtrop (May 12 2021 at 14:22):

Meven Lennon-Bertrand said:

Thanks for the detailed infos!
On a side-note though, I would say using tactics to construct terms as I do is not that harmful if you use tactics like case, exists, assumption and the like that behave mostly like refine with some term former (exists or split are inductive constructors, assumption a variable, case a match, intros lambda-abstractions…). But I agree that in general tactics can be quite dangerous.

this is true, but these are exactly those tactics which are not that hard to write in gallina right away. And one anyway has to think about the structure of the term when one starts to write proofs about it. So why not spend the extra effort when writing the definition rather than each time one writes a proof about it? Usually one writes more proofs than definitions, so shifting development time from definition time to proof time is rarely effective.


Last updated: Mar 28 2024 at 09:01 UTC