Make naming consistent with paper

src/Language/PlutusIR/Analysis/Equality.v

@@ -170,7 +170,7 @@ Definition string_eqb_eq := String.eqb_eq.
   Bool.eqb_true_iff
 : reflection.
 Definition andb_and : forall s t, s && t = true -> s = true /\ t = true.
-Proof. auto with reflection. Qed.
+Proof. debug auto with reflection. Qed.
 
 Ltac rewrite_eqbs := repeat (
   match goal with
@@ -400,8 +400,6 @@ Proof. eqb_eq_tac. Defined.
 #[export] Hint Resolve -> Kind_eqb_eq : reflection.
 #[export] Hint Resolve <- Kind_eqb_eq : reflection.
 
-(* TODO: This is not correct yet. Because we have computation in types, we can not merely rely
-  on syntactic equality checking. *)
 Fixpoint Ty_eqb (x y : Ty) : bool := match x, y with
   | Ty_Var X, Ty_Var Y => String.eqb X Y
   | Ty_Fun T1 T2, Ty_Fun T3 T4 => Ty_eqb T1 T3 && Ty_eqb T2 T4
@@ -505,12 +503,6 @@ Qed.
 #[export] Hint Resolve -> DTDecl_eqb_eq : reflection.
 #[export] Hint Resolve <- DTDecl_eqb_eq : reflection.
 
-
-
-
-
-
-
 Fixpoint Term_eqb (x y : Term) {struct x} : bool := match x, y with
   | Let rec bs t, Let rec' bs' t' => Recursivity_eqb rec rec'
       && list_eqb Binding_eqb bs bs'

src/Language/PlutusIR/Analysis/Purity.v

@@ -57,14 +57,14 @@ Inductive is_pure (Γ : ctx) : Term -> Type :=
       is_pure Γ (Var x)
 .
 
-Definition is_errorb (t : Term) : bool :=
+Definition dec_is_error (t : Term) : bool :=
   match t with
     | Error _ => true
     | _       => false
   end.
 
-Lemma is_errorb_not_is_error : forall t,
-  is_errorb t = false -> ~ is_error t.
+Lemma dec_is_error_not_is_error : forall t,
+  dec_is_error t = false -> ~ is_error t.
 Proof.
   intros t H.
   destruct t; intros H1; inversion H1.
@@ -90,7 +90,7 @@ Inductive pure_binding (Γ : ctx) : Binding -> Prop :=
       pure_binding Γ (TypeBind tvd ty)
 .
 
-Definition is_pure_binding (Γ : ctx) (b : Binding) : bool :=
+Definition dec_pure_binding (Γ : ctx) (b : Binding) : bool :=
     match b with
       | TermBind NonStrict vd t => true
       | TermBind Strict vd t    => dec_value t
@@ -99,6 +99,6 @@ Definition is_pure_binding (Γ : ctx) (b : Binding) : bool :=
     end
 .
 
-Lemma is_pure_binding_pure_binding : forall Γ b, is_pure_binding Γ b = true -> pure_binding Γ b.
+Lemma sound_dec_pure_binding : forall Γ b, dec_pure_binding Γ b = true -> pure_binding Γ b.
 Admitted.
 

src/Language/PlutusIR/Analysis/Value.v

@@ -139,27 +139,6 @@ Lemma dec_value_value : forall t,
   (dec_value t = true -> value t) /\
   (forall n, dec_neutral_value n t = true -> neutral_value n t).
 Proof.
-(*
-  intros t.
-  induction t.
-  all: split.
-  all: try destruct IHt.
-  all: match goal with
-    | H : _ |- dec_value _ = true -> _ => intro H_dec; auto; inversion H_dec
-    | _ => idtac
-  end.
-  - 
-  - 
-  all: auto; inversion H_dec.
-  - clear H0.
-    unfold dec_value in H_dec.
-    unfold dec_value' in H_dec.
-    fold dec_value' in H_dec.
-    repeat (rewrite_eqbs; destruct_ands).
-    apply V_Neutral.
-    apply NV_Apply; auto.
-*)
-
 Admitted.
 
 Lemma dec_neutral_value_neutral_value : forall n t, dec_neutral_value n t = true -> neutral_value n t.

src/Language/PlutusIR/Transform/Beta.v

@@ -10,28 +10,6 @@ From Coq Require Import
   Strings.String.
 Import ListNotations.
 
-(*
-
-This pass transforms beta redexes into let non-recs, so that the later inlining
-pass has more opportunities for inlining.
-
-Transforms repeated applications (not just repeated β-redexes), e.g.
-
-         $₃
-       /  \
-     $₂    t₃
-   /  \
-  $₁   t₂
-/  \                    =>      let nonrec x = t₁
-λx t₁                                      y = t₂
-|                                          z = t₃
-λy                              in t_body
-|
-λz
-|
-t_body
-
-*)
 
 Inductive lams : Term -> list Term -> list Binding -> Term -> Prop :=
 
@@ -58,17 +36,6 @@ Inductive betas  : Term -> list Term -> list Binding -> Term -> Prop :=
 .
 
 
-Goal forall v1 v2 τ1 τ2 t t1 t2,
-  betas
-    (Apply (Apply (LamAbs v1 τ1 (LamAbs v2 τ2 t)) t1) t2) []
-    [TermBind Strict (VarDecl v1 τ1) t1; TermBind Strict (VarDecl v2 τ2) t2] t.
-intros.
-repeat apply Betas_1.
-apply Betas_2.
-repeat apply Lams_1.
-apply Lams_2.
-Qed.
-
 Inductive beta : Term -> Term -> Prop :=
 
   | beta_multi : forall t bs bs' t_inner t_inner',