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.

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).

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

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)

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?

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

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).

(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.)

And probably an approach like this would also involve moving `hl ix P i Q`

into the constructors.

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.

Thanks y'all for the suggestions!

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?

@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.

if it's not a big hassle :smile:

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.... *).
```

(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`

.)

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.

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

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: Jun 24 2024 at 12:02 UTC