Experiments towards designing a good notational system for typing predicates

NotationExperiment.v

Require Import Bool.

(* The base type is largely irrelevant, so I'll use bool instead of a custom type of terms *)
(* Also, I am defining just one kind of relation in each "family" (rel1/rel2/rel),
  but in reality each family would have ~10 different, mutually defined predicates/relations *)

Inductive rel1 : bool -> bool -> Set :=
  | crel1_true : rel1 true false
  | crel1_neg b b' : rel1 (negb b) (negb b') -> rel1 b b'.

Inductive rel2 : bool -> bool -> Set :=
  | crel2_true : rel2 true false
  | crel2_false : rel2 false true.

Inductive tag : Set :=
  | o : tag (* one *)
  | tw : tag. (* two *)
(* we would ideally want short tags because they are being used a lot, but would rather want to avoid polluting the namespaces… *)

Class Rel (t : tag) := rel : bool -> bool -> Type.
Class RelProp {t : tag} `(R : Rel t) := {
    rel_true : rel true false ;
    rel_neg  b b' : rel (negb b) (negb b') -> rel b b'}.

Arguments rel _ {_}.

Module TaggedNotation.

  Notation "[ |-[ t  ] b ~ b' ]" := (rel t b b') (t, b, b' at level 40).

End TaggedNotation.

Module UntaggedNotation.

  Notation "[ |- b ~ b' ]" := (rel _ b b') (b, b' at level 40).

End UntaggedNotation.

Module TagRelInst1.

  #[export] Instance Rel1 : Rel o := rel1.
  #[export, refine] Instance RelProp1 : RelProp Rel1 := {}.
  Proof.
    - econstructor.
    - intros.
      now econstructor. 
  Defined.

End TagRelInst1.

Module TagRelInst2.

  #[export] Instance Rel2 : Rel tw := rel2.
  #[export, refine] Instance RelProp2 : RelProp Rel2 := {}.
  Proof.
    - econstructor.
    - intros ? ? H.
      inversion H ; subst ; clear H.
      all: destruct b, b' ; cbn in * ; try solve [congruence].
      all: cbn ; now econstructor.
  Defined.

End TagRelInst2.

Section TestingGen.
  Context `{R : Rel} `{HR : !RelProp R}.
  Import UntaggedNotation.

  Lemma rel_false : [ |- false ~ true ].
  Proof.
    apply rel_neg.
    cbn.
    now apply rel_true.
  Qed.

End TestingGen.

Section TestingSpecific.
  Import TagRelInst1 UntaggedNotation.

  Lemma rel1_false : [ |- false ~ true ].
  Proof.
    apply rel_false.
  Restart.
    econstructor. (* not ideal: after econstructor, the notation is lost! *)
    Fail change [ |- _ ~ _ ]. (*this is annoying: change does not use unification *)
    change [|- negb false ~ negb true]. (*this works*)
    Undo.
    refine (_ : [|- _ ~ _]). (*at least this works*)
    cbn.
    eapply rel_true. (* and the generically-proven lemmas work*)
  Qed.

End TestingSpecific.

Section TestingGen.
  Context {t : tag} `{R : Rel t} `{HR : !RelProp R}.
  Import TaggedNotation.

  Lemma relt_false : [ |-[ t ] false ~ true ].
  Proof.
    apply rel_neg.
    cbn.
    now apply rel_true.
  Qed.

End TestingGen.

Section TestingSpecific.

  Import TagRelInst1 TaggedNotation.

  Lemma rel1t_false : [ |-[ o ] false ~ true ].
  Proof.
    apply relt_false.
  Restart.
    econstructor. (* again, after econstructor, the notation is lost *)
    refine (_ : [|-[o] _ ~ _]).
    cbn.
    eapply rel_true.
  Qed.

End TestingSpecific.

Section TestingRelation.

  Import TagRelInst1 TagRelInst2 TaggedNotation.
  Context {t : tag} `{R : Rel t} `{HR : !RelProp R}.

  Lemma impl1gen b b' : [|-[ o ] b ~ b'] -> [|-[ t ] b ~ b'].
  Proof.
    induction 1.
    - eapply rel_true.
    - now eapply rel_neg.
  Qed.

  Lemma impl2gen b b' : [|-[ tw ] b ~ b'] -> [|-[ t ] b ~ b'].
  Proof.
    destruct 1.
    - eapply rel_true.
    - eapply rel_neg.
      cbn.
      eapply rel_true.
  Qed. 

End TestingRelation.

Definition impl12 := @impl1gen _ _ TagRelInst2.RelProp2.
Definition impl21 := @impl1gen _ _ TagRelInst2.RelProp2.