Finish renaming

syntax.sig

@@ -1,17 +1,29 @@
 nat  : Type
+PTm(VarPTm) : Type
 Tm(VarTm) : Type
 PTag : Type
 TTag : Type
+bool : Type
 
 PL : PTag
 PR : PTag
 TPi : TTag
 TSig : TTag
+
+PAbs : (bind PTm in PTm) -> PTm
+PApp : PTm -> PTm -> PTm
+PPair : PTm -> PTm -> PTm
+PProj : PTag -> PTm -> PTm
+PConst : TTag -> PTm
+PUniv : nat -> PTm
+PBot : PTm
+
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
-Const : TTag -> Tm
 Univ : nat -> Tm
-Bot : Tm
+BVal : bool -> Tm
+Bool : Tm
+If : Tm -> Tm -> Tm -> Tm

theories/compile.v

@@ -15,11 +15,14 @@ Module Compile.
     | Pair a b => Pair (F a) (F b)
     | Proj t a => Proj t (F a)
     | Bot => Bot
+    | If a b c => App (App (F a) (F b)) (F c)
+    | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero)))
+    | Bool => Bool
     end.
 
   Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
     F (ren_Tm ξ a)= ren_Tm ξ (F a).
-  Proof. move : m ξ. elim : n  / a => //=; scongruence. Qed.
+  Proof. move : m ξ. elim : n  / a => //=; hauto lq:on. Qed.
 
   #[local]Hint Rewrite Compile.renaming : compile.
 
@@ -33,6 +36,8 @@ Module Compile.
     - hauto lq:on rew:off.
     - hauto lq:on.
     - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    - hauto lq:on rew:off.
+    - hauto lq:on rew:off.
   Qed.
 
   Lemma substing n b (a : Tm (S n)) :

theories/diagram.txt

@@ -18,3 +18,25 @@ a0 >> a1
 |     |
 v     v
 b0 >> b1
+
+
+prov x (x, x)
+
+prov x b
+
+
+a => b
+
+prov x a
+
+prov y b
+
+prov x c
+prov y c
+
+extract c = x
+extract c = y
+
+prov x b
+
+pr