✔ Typeclass instance for mutually inductive types · Coq users

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

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?

Kenji Maillard (Dec 06 2022 at 09:59):

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.

Meven Lennon-Bertrand (Dec 06 2022 at 10:04):

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.

Kenji Maillard (Dec 06 2022 at 10:18):

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

Tan Yee Jian (Dec 07 2022 at 00:57):

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

Tan Yee Jian (Dec 07 2022 at 01:25):

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!

Stream: Coq users

Topic: ✔ Typeclass instance for mutually inductive types

Tan Yee Jian (Dec 06 2022 at 06:57):

Kenji Maillard (Dec 06 2022 at 09:59):

Meven Lennon-Bertrand (Dec 06 2022 at 10:04):

Kenji Maillard (Dec 06 2022 at 10:18):

Tan Yee Jian (Dec 07 2022 at 00:57):

Tan Yee Jian (Dec 07 2022 at 01:25):

Notification Bot (Dec 07 2022 at 01:25):