## 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_expr`s 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 `nat`s. The `arith_expr`s 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