Stream: Coq users

Topic: ✔ Typeclass instance for mutually inductive types


view this post on Zulip Tan Yee Jian (Dec 06 2022 at 06:57):

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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 |}.

view this post on Zulip 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:

view this post on Zulip 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!

view this post on Zulip Notification Bot (Dec 07 2022 at 01:25):

Tan Yee Jian has marked this topic as resolved.


Last updated: Jun 15 2024 at 08:01 UTC