GenTree pedagogical example · math-comp users

I sometimes advise people to use GenTree.tree to get their choiceType/countableType structures for their custom datatypes. However, there is seemingly no "pedagogical" example walking through the steps to use GenTree.tree for this, and while MCB mentions GenTree.tree there's no example there either. Is there any code in a MC-related projects using GenTree.tree we could use as a standard pointer?

Ana de Almeida Borges (Oct 04 2023 at 21:08):

It appears early, so there should be no need to understand a lot of context for the code to make sense

Karl Palmskog (Oct 04 2023 at 21:27):

@Ana de Almeida Borges thanks, here is a minimized example that does just enough to get the canonicals we want (in MathComp 1.17). Would it be OK to put this snippet under some permissive license so people can copy and adapt without bothering too much with licensing stuff?

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Formulas.

Definition VarName : Type := nat.

Record signature : Type := Signature {
  ConstName : finType;
  PredName : finType;
  arity : PredName -> nat;
}.

Variable sig : signature.

Inductive term : Type :=
  | Var : VarName -> term
  | Const : ConstName sig -> term.

Definition term_code (t : term) : nat + 'I_#|ConstName sig| :=
  match t with
  | Var x => inl x
  | Const c => inr (enum_rank c)
  end.

Definition term_decode (ct : nat + 'I_#|ConstName sig|) : term :=
  match ct with
  | inl n => Var n
  | inr i => Const (enum_val i)
  end.

Lemma term_codeK : cancel term_code term_decode.
Proof. by case => [// | /= ?]; rewrite enum_rankK. Qed.

Definition term_eqMixin := CanEqMixin term_codeK.
Canonical term_eqType := EqType term term_eqMixin.
Definition term_choiceMixin := CanChoiceMixin term_codeK.
Canonical term_choiceType := ChoiceType term term_choiceMixin.
Definition term_countMixin := CanCountMixin term_codeK.
Canonical term_countType := CountType term term_countMixin.

Inductive formula : Type :=
  | T : formula
  | Pred : forall P : PredName sig, (arity P).-tuple term -> formula
  | Conj : formula -> formula -> formula
  | Diam : formula -> formula
  | All : VarName -> formula -> formula.

Fixpoint formula_code (A : formula)
    : GenTree.tree (option (PredName sig * seq term)) :=
  match A with
  | T => GenTree.Leaf None
  | Pred P ts => GenTree.Leaf (Some (P, val ts))
  | Conj A B => GenTree.Node 0 [:: formula_code A; formula_code B]
  | Diam A => GenTree.Node 1 [:: formula_code A]
  | All x A => GenTree.Node x.+2 [:: formula_code A]
  end.

Fixpoint formula_decode
    (c : GenTree.tree (option (PredName sig * seq term))) : formula :=
  match c with
  | GenTree.Leaf None => T
  | GenTree.Leaf (Some (P, vts)) =>
      if size vts == arity P then
        @Pred P (insubd [tuple of nseq (arity P) (Var 0)] vts)
      else T
  | GenTree.Node 0 [:: c1; c2] => Conj (formula_decode c1) (formula_decode c2)
  | GenTree.Node 1 [:: c1] => Diam (formula_decode c1)
  | GenTree.Node k.+2 [:: c1] => All k (formula_decode c1)
  | GenTree.Node _ _ => T
  end.

Lemma formula_codeK : cancel formula_code formula_decode.
  elim => //=.
 - move=> P ts.
   rewrite /insubd insubT; first by rewrite size_tuple.
   move=> sizek; rewrite size_tuple eqxx /=.
   by congr Pred; apply/val_eqP.
 - by move=> A -> B ->.
 - by move=> A ->.
 - by move=> x A ->.
Qed.

Definition formula_eqMixin := CanEqMixin formula_codeK.
Canonical formula_eqType := EqType formula formula_eqMixin.
Definition formula_choiceMixin := CanChoiceMixin formula_codeK.
Canonical formula_choiceType := ChoiceType formula formula_choiceMixin.
Definition formula_countMixin := CanCountMixin formula_codeK.
Canonical formula_countType := CountType formula formula_countMixin.

End Formulas.

Karl Palmskog (Oct 04 2023 at 21:30):

(unfortunately it'd need somewhat nontrivial adaptation to work on MC2, so not bothering with that right now)

Enrico Tassi (Oct 05 2023 at 05:30):

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Formulas.

Definition VarName : Type := nat.

Record signature : Type := Signature {
  ConstName : finType;
  PredName : finType;
  arity : PredName -> nat;
}.

Variable sig : signature.

Inductive term : Type :=
  | Var : VarName -> term
  | Const : ConstName sig -> term.

Definition term_code (t : term) : nat + 'I_#|ConstName sig| :=
  match t with
  | Var x => inl x
  | Const c => inr (enum_rank c)
  end.

Definition term_decode (ct : nat + 'I_#|ConstName sig|) : term :=
  match ct with
  | inl n => Var n
  | inr i => Const (enum_val i)
  end.

Lemma term_codeK : cancel term_code term_decode.
Proof. by case => [// | /= ?]; rewrite enum_rankK. Qed.

HB.instance Definition _ := Countable.copy term (can_type term_codeK).

HB.about term.

Inductive formula : Type :=
  | T : formula
  | Pred : forall P : PredName sig, (arity P).-tuple term -> formula
  | Conj : formula -> formula -> formula
  | Diam : formula -> formula
  | All : VarName -> formula -> formula.

Fixpoint formula_code (A : formula)
    : GenTree.tree (option (PredName sig * seq term)) :=
  match A with
  | T => GenTree.Leaf None
  | Pred P ts => GenTree.Leaf (Some (P, val ts))
  | Conj A B => GenTree.Node 0 [:: formula_code A; formula_code B]
  | Diam A => GenTree.Node 1 [:: formula_code A]
  | All x A => GenTree.Node x.+2 [:: formula_code A]
  end.

Fixpoint formula_decode
    (c : GenTree.tree (option (PredName sig * seq term))) : formula :=
  match c with
  | GenTree.Leaf None => T
  | GenTree.Leaf (Some (P, vts)) =>
      if size vts == arity P then
        @Pred P (insubd [tuple of nseq (arity P) (Var 0)] vts)
      else T
  | GenTree.Node 0 [:: c1; c2] => Conj (formula_decode c1) (formula_decode c2)
  | GenTree.Node 1 [:: c1] => Diam (formula_decode c1)
  | GenTree.Node k.+2 [:: c1] => All k (formula_decode c1)
  | GenTree.Node _ _ => T
  end.

Lemma formula_codeK : cancel formula_code formula_decode.
  elim => //=.
 - move=> P ts.
   rewrite /insubd insubT; first by rewrite size_tuple.
   move=> sizek; rewrite size_tuple eqxx /=.
   by congr Pred; apply/val_eqP.
 - by move=> A -> B ->.
 - by move=> A ->.
 - by move=> x A ->.
Qed.

HB.instance Definition _ := Countable.copy formula (can_type formula_codeK).

HB.about formula.

End Formulas.

Enrico Tassi (Oct 05 2023 at 05:33):

The main change is that declaring instances by providing a cancellation lemma can be dome in one go,
by telling HB to copy a structure on a new type (term here) via the can_type feather factory (which links term to a known countType via a can lemma) :

HB.instance Definition _ := Countable.copy term (can_type term_codeK).

In one go you get eqType, choiceType and countType (and whatever in the future we may introduce below countable).

Ana de Almeida Borges (Oct 05 2023 at 19:08):

@Karl Palmskog Sure, everyone can feel free to use and adapt this snipet however they like

Stream: math-comp users