Stream: Coq users

Topic: Inductive relation over another relation

Audrey Seo (Dec 09 2022 at 03:18):

Hi! I'm trying to create some relation over Hoare proof trees. For a minimal example, suppose we have

Inductive imp :=
| Skip
| Seq (i1 i2: imp).

Inductive MyProp := (* something whose equality is not decidable *).

Inductive hl : MyProp -> imp -> MyProp -> Type :=
| hl_skip :
  forall (P: MyProp),
    hl P Skip P
| hl_seq :
  forall (P Q R: MyProp) (i1 i2: imp),
  hl P i1 Q ->
  hl Q i2 R ->
  hl P (Seq i1 i2) R
| hl_consequence :
  forall (P P' Q Q': MyProp) (i: imp),
  (P' -> P) ->
  (Q -> Q') ->
  hl P i Q ->
  hl P' i Q'.

Inductive myprop_relation : MyProp -> Prop := (* some relation *).

Inductive hl_myprop_relation: forall (P: MyProp) (i: imp) (Q: MyProp), hl P i Q -> Prop :=
| hl_myprop_skip :
  forall P,
    myprop_relation P ->
    hl_myprop_relation P Skip P (hl_skip P)
| hl_myprop_seq :
  forall P Q R i1 i2,
  forall (hl1: hl P i1 Q)
              (hl2: hl Q i2 R),
    myprop_relation P ->
    myprop_relation Q ->
    myprop_relation R ->
    hl_myprop_relation P i1 Q hl1 ->
    hl_myprop_relation Q i2 R hl2 ->
    hl_myprop_relation P (Seq i1 i2) R (hl_seq P Q R i1 i2 hl1 hl2)
| hl_myprop_consequence :
  forall P P' Q Q' i,
  forall (implies1: P' -> P) (implies2: Q -> Q') (H: hl P i Q)
    myprop_relation P ->
    myprop_relation Q ->
    myprop_relation P' ->
    myprop_relation Q' ->
    hl_myprop_relation P i Q H ->
    hl_myprop_relation P' i Q' (hl_consequence P P' Q Q' i implies1 implies2 H).

But when I'm doing induction over the hl relation, if I use inversion on hl_myprop_consequence, I get nasty dependent type equalities for cases that are recursive. For example, if I try to use inversion on an instance of hl_myprop_relation P (Seq i1 i2) R (hl_seq P Q R i1 i2 hl1 hl2), I get an equality like

hl4: hl P i1 R
hl5: hl R i2 Q
H: existT (fun P: MyProp => {R: MyProp & {i1: imp & hl P i1 R}}) P
  (existT (fun R: MyProp => {i1: imp & hl P i1 R}) R
    (existT (fun i1 => hl P i1 R) i1 hl4)) =
      existT (fun P: MyProp => {R: MyProp & {i1: imp & hl P i1 R}}) P
        (existT (fun R: MyProp => {i1: imp & hl P i1 R}) R
          (existT (fun i1 => hl P i1 R) i1 hl1))

and inversion_sigma doesn't produce anything that I can do anything with.

How can I avoid these dependent equalities? I tried changing hl so it injected into Prop instead of Type, but then I was unable to use induction on hl at all.

Li-yao (Dec 09 2022 at 10:03):

You can try dependent destruction https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/reasoning-inductives.html#dependent-induction-examples

Another way may be to make P and Q parameters instead of indices

hl_myprop_relation (P Q : MyProp) : forall (i : imp) -> hl P i Q -> Prop

This helps more with destruction rather than induction, but it has the advantage of not assuming the UIP axiom (which dependent destruction does).

Paolo Giarrusso (Dec 09 2022 at 13:13):

If UIP is a concern, IIRC one can also use replacement tactics from Coq-equations...

Anton Golov (they/them) (Dec 09 2022 at 13:55):

To suggest a different approach: my experience has been that in cases like this it may be easier to add an index to everything and define the relations using that index, so that hl can go to Prop. It's a little less elegant, but much easier to work with (IMHO)

Paolo Giarrusso (Dec 09 2022 at 14:54):

Which index do you have in mind? Like index/parameterize hl over extraReq : MyProp -> Prop, and then instantiate it with (fun _ => True) or myProp_relation?

Paolo Giarrusso (Dec 09 2022 at 14:55):

Seems this version works, but maybe you meant something else even better?

Anton Golov (they/them) (Dec 09 2022 at 15:05):

Oh, that's also possible; I was thinking more in the direction of something like...

Inductive Ix := (* Some set that captures what is currently expressed in myprop_relation *)
Inductive imp :=
| Skip
| Seq (i1 i2: imp).

Inductive MyProp (ix : Ix) := (* something whose equality is not decidable *).

(* Or perhaps ix and jx so that you can control them separately. *)
Inductive hl ix : MyProp ix -> imp -> MyProp ix -> Prop :=
| hl_skip :
  forall (P: MyProp ix),
    hl ix P Skip P
| ...

Inductive myprop_relation : Ix -> Prop := (* some relation *).

Inductive hl_myprop_relation: forall (ix : Ix) (P: MyProp ix) (i: imp) (Q: MyProp ix), hl ix P i Q -> Prop :=
| hl_myprop_skip :
  forall P,
    myprop_relation ix ->
    hl_myprop_relation P Skip P (hl_skip P)
| ...

This requires being able to in some sense bake whatever property myprop_relation is checking into MyProp up front, which might not be ideal, but it lets you avoid reasoning about any kind of dependent destruction (I think).

Anton Golov (they/them) (Dec 09 2022 at 15:07):

(Probably you do want separate ix and jx for P and Q here, though, and unfortunately it works out to be a whole lot of indices. On the other hand, I think some can be moved out of the signature of hl_myprop_relation and into the individual constructors.)

Anton Golov (they/them) (Dec 09 2022 at 15:12):

And probably an approach like this would also involve moving hl ix P i Q into the constructors.

Anton Golov (they/them) (Dec 09 2022 at 15:12):

Basically, my experience has been that introducing indices like this and specifying conditions on them tends to work better than dependent pattern matching, despite it feeling somewhat roundabout. I'm very much not a Coq expert, though.

Audrey Seo (Dec 13 2022 at 00:22):

Thanks y'all for the suggestions!

Audrey Seo (Dec 13 2022 at 00:25):

Anton Golov (they/them) said:

(Probably you do want separate ix and jx for P and Q here, though, and unfortunately it works out to be a whole lot of indices. On the other hand, I think some can be moved out of the signature of hl_myprop_relation and into the individual constructors.)

I was wondering if you could give more of an explanation of what an index would look like? Or maybe some examples?

Paolo Giarrusso (Dec 13 2022 at 01:00):

@Audrey Seo would you be willing to elaborate on myprop_relation? If yes, it might help understand if this "index" strategy is a good fit and how to apply it.

Paolo Giarrusso (Dec 13 2022 at 01:00):

if it's not a big hassle :smile:

Audrey Seo (Dec 13 2022 at 05:00):

Yeah sure @Paolo Giarrusso! I didn't want to bog down the original code with too many details.
Suppose we have arithmetic expressions

Inductive arith_expr :=
| Const (n: nat)
| Var (x: string)
| Plus (a1 a2: arith_expr).

So MyProp actually has the form

Inductive MyProp :=
| UnaryProp (f: nat -> Prop) (a: arith_expr)
| BinaryProp (f: nat -> nat -> Prop) (a1 a2: arith_expr)
| AndProp (m1 m2: MyProp).

And myprop_relation says that all variables in the arith_exprs of a MyProp are "in scope," i.e., contained in some list of in-scope variables

Inductive all_vars_in_scope : list string -> arith_expr -> Prop :=
| AllVarsConst :
  forall (idents: list string) (n: nat),
   all_vars_in_scope idents (Const n)
| AllVarsVar :
  forall (idents: list string) (x: string),
   In x idents ->
   all_vars_in_scope idents (Var x)
| AllVarsPlus :
  forall (idents: list string) (a1 a2: arith_expr),
    all_vars_in_scope idents a1 ->
    all_vars_in_scope idents a2 ->
    all_vars_in_scope idents (Plus a1 a2).

Inductive myprop_relation: list string -> MyProp -> Prop :=
| MyPropUnary :
  forall (idents: list string) (f: nat -> Prop) (a: arith_expr),
    all_vars_in_scope idents a ->
    myprop_relation idents (UnaryProp f a)
| MyPropBinary :
  forall (idents: list string) (f: nat -> nat -> Prop) (a1 a2: arith_expr),
    all_vars_in_scope idents a1 ->
    all_vars_in_scope idents a2 ->
    myprop_relation idents (BinaryProp f a1 a2)
| MyPropAnd :
  forall (idents: list string) (m1 m2: MyProp),
    myprop_relation idents m1 ->
    myprop_relation idents m2 ->
    myprop_relation idents (AndProp m1 m2).

And then the list of strings would be threaded through hl_myprop_relation in the same way:

Inductive hl_myprop_relation (idents: list string): forall (P: MyProp) (i: imp) (Q: MyProp), hl P i Q -> Prop :=
| hl_myprop_skip :
  forall P,
    myprop_relation idents P ->
    hl_myprop_relation idents P skip P (hl_skip P)
(* etc.... *).

Audrey Seo (Dec 13 2022 at 05:02):

(The whole point of MyProp, by the way, is to abstract over propositions about nats. The arith_exprs can be evaluated to nat.)

Gaëtan Gilbert (Dec 13 2022 at 07:52):

It seems like you can equivalently write hl_myprop_relation as a fixpoint, ie

Fixpoint hl_myprop_relation (idents: list string) (P: MyProp) (i: imp) (Q: MyProp) (h:hl P i Q) : Prop :=
  match hl with
  | hl_skip P => myprop_relation idents P
  | hl_seq P Q R i1 i2 hl1 hl2 => myprop_relation P /\ myprop_relation Q /\ myprop_relation R /\ hl_myprop_relation _ _ _ hl1 /\ hl_myprop_relation _ _ _ hl2
  | ...
  end.

then either use that everywhere, or if you want to eg do inductions over hl_myprop_relation then keep the inductive, instead of a fixpoint use a nonrecursive definition (ie the recursive occurences refer to the inductive) with a proof that it's equivalent to the inductive, and use the equivalence instead of the inversion tactic.

Audrey Seo (Dec 13 2022 at 23:26):

Ooh, interesting! I'll have to try this out...

Anton Golov (they/them) (Dec 21 2022 at 10:31):

Oh, I see what you mean now. I missed the P and Q hiding inside the definition of hl earlier, and I agree with Paolo's suggestion of using a predicate and passing it to hl. My initial suggestion of making MyProp indexed by something (in this case the free variables) could also work but I think you'll still end up having to do dependent pattern matching, which may not be ideal. A more extreme approach is to make a datatype that describes the hl_consequence steps and then restrict that, but it seems a bit roundabout. Sorry for the confusion!

Last updated: Oct 05 2023 at 02:01 UTC