walker (Dec 11 2022 at 10:22): 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 ?
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).
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
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 :=
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
walker (Dec 11 2022 at 11:51):I also cannot recognize this part as v return v = pser ops x -> list Bit with
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: Apr 19 2024 at 00:02 UTC