Stream: Coq users

Topic: Convince coq that a function decreases argument


view this post on Zulip walker (Dec 11 2022 at 10:22):

I am building an interface for partially serializing an instance type K into bits as follows:

Inductive Bit : Type :=
| Bit0 : Bit
| Bit1: Bit.

Record hasPSerDe {T} := {
    pser: T -> Bit * option T;
    pdeser: Bit -> option T -> T;
    pdeser_pser: forall x y b, (b, y) = pser x -> x = pdeser b y;
    pser_pdeser: forall x y b, x = pdeser b y -> (b, y) = pser x
}.

The there is one more property I cannot figure out how to say that is
if

let (b, y) = pser ops x

then y must be less than x

This becomes important when I have to deal with functions like the one below:

Fixpoint consume {T} (ops: @hasPSerDe T) (x: T) : list Bit :=
let (bit, ox) := pser ops x in
match ox with
| Some x' => cons bit (consume ops x')
| None =>   cons bit nil
end.

There is noething that implies that x' is structurally smaller than x.

How can I encode this property and how to let coq use it ?

view this post on Zulip Gaëtan Gilbert (Dec 11 2022 at 10:31):

something like this?

Record hasPSerDe {T} := {
    pser: T -> Bit * option T;
    pdeser: Bit -> option T -> T;
    pdeser_pser: forall x y b, (b, y) = pser x -> x = pdeser b y;
    pser_pdeser: forall x y b, x = pdeser b y -> (b, y) = pser x;
    pser_decrease x y :=  exists b, (b, Some x) = pser y;
    pser_terminates : well_founded pser_decrease;
  }.

Fixpoint consume_aux {T} (ops: @hasPSerDe T) (x: T) (a:Acc (pser_decrease ops) x) : list Bit :=
  match pser ops x as v return v = pser ops x -> list Bit with
    | (bit, ox) =>
        match ox with
        | Some x' =>
            fun e : (bit, Some x') = pser ops x =>
              let p := ex_intro (fun bit => (bit, Some x') = pser ops x) bit e in
              cons bit (consume_aux ops x' (Acc_inv a x' p))
        | None => fun _ => cons bit nil
        end
  end eq_refl.

Definition consume {T} ops x := @consume_aux T ops x (pser_terminates ops x).

view this post on Zulip Gaëtan Gilbert (Dec 11 2022 at 10:36):

and probably you use something like https://github.com/coq/coq/blob/master/theories/Wellfounded/Inclusion.v to prove pser_terminates from some other relation on T when you want to instantiate the record

view this post on Zulip walker (Dec 11 2022 at 11:40):

This is a neat trick (that I am still trying to comprehend), but I didn't notice the := part in pser_decrease x y :=

view this post on Zulip walker (Dec 11 2022 at 11:51):

by the way the snippet does not work in empty coq file, it complains about missing case None, None

view this post on Zulip walker (Dec 11 2022 at 11:51):

I also cannot recognize this part as v return v = pser ops x -> list Bit with

view this post on Zulip Gaëtan Gilbert (Dec 11 2022 at 12:06):

full file (modified a bit to provide an example with positive, as positive refuses deserialization with Bit0 None)

Inductive Bit : Type :=
| Bit0 : Bit
| Bit1: Bit.

Record hasPSerDe {T} := {
    pser: T -> Bit * option T;
    pdeser: Bit -> option T -> option T;
    pdeser_pser: forall x y b, (b, y) = pser x -> Some x = pdeser b y;
    pser_pdeser: forall x y b, Some x = pdeser b y -> (b, y) = pser x;
    pser_decrease x y :=  exists b, (b, Some x) = pser y;
    pser_terminates : well_founded pser_decrease;
  }.
Arguments hasPSerDe _ : clear implicits.

Fixpoint consume_aux {T} (ops: hasPSerDe T) (x: T) (a:Acc (pser_decrease ops) x) : list Bit :=
  match pser ops x as v return v = pser ops x -> list Bit with
    | (bit, ox) =>
        match ox with
        | Some x' =>
            fun e : (bit, Some x') = pser ops x =>
              let p := ex_intro (fun bit => (bit, Some x') = pser ops x) bit e in
              cons bit (consume_aux ops x' (Acc_inv a x' p))
        | None => fun _ => cons bit nil
        end
  end eq_refl.

Definition consume {T} ops x := @consume_aux T ops x (pser_terminates ops x).

Require Import BinNums Wellfounded.

Definition pos_subterm x y :=
  match y with
  | xI y' | xO y' => x = y'
  | xH => False
  end.

Lemma pos_subterm_wf : well_founded pos_subterm.
Proof.
  intros x;induction x as [x IHx|x IHx|];constructor;intros y Hy;simpl in Hy;subst;auto.
  destruct Hy.
Defined.

Definition pos_pser : hasPSerDe positive.
Proof.
  refine {| pser p :=
             match p with
             | xI p' => (Bit1, Some p')
             | xO p' => (Bit0, Some p')
             | xH => (Bit1, None)
             end;

           pdeser b p :=
             match b, p with
             | Bit1, Some p => Some (xI p)
             | Bit0, Some p => Some (xO p)
             | Bit1, None => Some xH
             | Bit0, None => None
             end;
         |}.
  - abstract (intros x y b H; destruct b,x,y;simpl in *;congruence).
  - abstract (intros x y b H; destruct b,x,y;simpl in *;congruence).
  - abstract (eapply wf_incl;[|exact pos_subterm_wf];
              intros x y [b H];
              destruct y;simpl;congruence).
Defined.

this works on my machine, tested 8.11 and 8.16


Last updated: Jun 17 2024 at 22:01 UTC