Hi all! I am trying to define reflection for a inductive type using a type class. I have come up with a small example on where I am stuck (the tree isn't really a tree):

```
Inductive reflectProp (P : Prop) : bool -> Prop :=
| reflectP : P -> reflectProp P true
| reflectF : ~ P -> reflectProp P false.
Class ReflectEq A := {
eqb : A -> A -> bool ;
eqb_spec : forall x y : A, reflectProp (x = y) (eqb x y) (* Prevent using reflect in computational content *)
}.
Inductive tree :=
| tree_cons : node -> tree
with node :=
| node_nil
| node_tree : tree -> node.
Fixpoint eqb_tree (t t': tree) :=
match t, t' with
| tree_cons n, tree_cons n' => eqb_node n n'
end
with eqb_node n n' :=
match n, n' with
| node_nil, node_nil => true
| node_tree t, node_tree t' => eqb_tree t t'
| _, _ => false
end.
#[global] Instance reflect_tree : ReflectEq tree.
Proof.
```

Any idea how I can proceed with the proof? I have tried to do it by mutual induction, with the help of a reflection lemma `eqb_eq`

:

```
Lemma eqb_eq {A} `{ReflectEq A} (x y : A) : x == y -> x = y.
Proof.
elim: eqb_spec; auto.
discriminate.
Qed.
Scheme tree_recp := Induction for tree Sort Set with
node_recp := Induction for node Sort Set.
Combined Scheme tree_node_mutrecp from tree_recp, node_recp.
#[global] Instance reflect_tree : ReflectEq tree.
Proof.
refine {| eqb := eqb_tree |}.
set (P := fun t => forall t', reflectProp (t = t') (eqb_tree t t')).
set (P0 := fun t => forall t', reflectProp (t = t') (eqb_node t t')).
cut ((forall t: tree, P t) × (forall n: node, P0 n)).
intros [Htree Hnode].
- apply Htree.
- apply tree_node_mutrecp.
-- intros. unfold P. intros. destruct t'; try discriminate.
simpl. unfold P0 in H. destruct (eqb_node n n0) eqn:E.
+ constructor. f_equal. apply eqb_eq. (*stuck*)
```

The error message:

```
Unable to satisfy the following constraints:
In environment:
P := fun t : tree => forall t' : tree, reflectProp (t = t') (eqb_tree t t') : tree -> Prop
P0 := fun t : node => forall t' : node, reflectProp (t = t') (eqb_node t t') : node -> Prop
n : node
H : forall t' : node, reflectProp (n = t') (eqb_node n t')
n0 : node
E : eqb_node n n0 = true
?H : "ReflectEq node"
```

Which is what I was hoping the mutual induction would prove. This arises because I have to define both `ReflectEq tree`

and `ReflectEq node`

simultaneously. How can I do that?

HI @Tan Yee Jian , I think your proof would be easier if you were to do a case analysis on an adequate instantiation of your inductive hypothesis (in the case your are struck with, this means destructing `(H n0)`

instead of `eqb_node n n0`

).

On some details: I find it helpful to unfold `P,P0`

just after applying the induction principle (`apply tree_node_mutrecp; unfold P,P0.`

) and the `constructor`

and `congruence`

tactics can be your friend to factor the proof.

I was sniped by Kenji, but just to be a bit more precise: when you have some `H: reflectProp P b`

, doing case analysis on `H`

gives you two cases, one where `P`

holds and `b`

is replaced by `true`

, and the other where `~P`

holds and `b`

is replaced by `false`

. So it does case-split on `b`

, but on top of that also gives you the corresponding proposition directly for you to use.

Also in terms of code organization it might be useful to have both instances on trees and nodes. In that case, you could first prove your intermediate lemma and then define the two instances.

```
Lemma rptreenode : (forall t t', reflectProp (t = t') (eqb_tree t t')) * (forall t t', reflectProp (t = t') (eqb_node t t')).
Proof.
apply tree_node_mutrecp.
(* Here goes the main proof *)
Qed.
#[global] Instance reflect_tree : ReflectEq tree :=
{| eqb := eqb_tree ; eqb_spec := fst rptreenode |}.
#[global] Instance reflect_node : ReflectEq node :=
{| eqb := eqb_node ; eqb_spec := snd rptreenode |}.
```

Thank you all for the useful hints! Really appreciate them, I will give them a try now. :happy:

Oh my, that was insanely helpful, especially the tip on destructing the "larger" hypothesis `destruct (H n0)`

which gave me a lot more to work with, and the organization of code by a intermediate lemma, Coq can match the induction principle much better that way. Very happy! Thanks, Meven and Kenji, once again!

Tan Yee Jian has marked this topic as resolved.

Last updated: Jun 15 2024 at 08:01 UTC