Skip to content

Instantly share code, notes, and snippets.

@MevenBertrand
Last active November 26, 2022 17:02
Show Gist options
  • Save MevenBertrand/ab0e0a75d62599877576a15d85601c35 to your computer and use it in GitHub Desktop.
Save MevenBertrand/ab0e0a75d62599877576a15d85601c35 to your computer and use it in GitHub Desktop.
Experiments towards designing a good notational system for typing predicates
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment