[WIP] add PER

theories/Core/Semantic/PER.v

@@ -0,0 +1,33 @@
+From Coq Require Import Relations.
+
+From Mcltt Require Import Base.
+From Mcltt Require Import Domain.
+From Mcltt Require Import Readback.
+From Mcltt Require Import Syntax.
+From Mcltt Require Import System.
+
+Notation "'Dom' a ≈ b ∈ R" := (R a b) (in custom judg at level 90, a custom domain, b custom domain, R constr).
+
+Generalizable All Variables.
+
+Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
+
+Definition per_top : relation domain_nf := fun m n => (forall s, exists L, {{ Rnf m in s ↘ L }} /\ {{ Rnf n in s ↘ L }}).
+
+Definition per_top_typ : relation domain := fun a b => (forall s, exists C, {{ Rtyp a in s ↘ C }} /\ {{ Rtyp b in s ↘ C }}).
+
+Inductive per_nat : relation domain :=
+| per_nat_zero : {{ Dom zero ≈ zero ∈ per_nat }}
+| per_nat_succ :
+  `( {{ Dom m ≈ n ∈ per_nat }} ->
+     {{ Dom succ m ≈ succ n ∈ per_nat }} )
+| per_nat_neut :
+  `( {{ Dom m ≈ n ∈ per_bot }} ->
+     {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} )
+.
+
+Inductive per_ne : relation domain :=
+| per_ne_neut :
+  `( {{ Dom m ≈ n ∈ per_bot }} ->
+     {{ Dom ⇑ a m ≈ ⇑ a' n ∈ per_ne }} )
+.