style: (wip) use Prop wherever possible, pt. 2

Plfl/DeBruijn.lean

@@ -301,14 +301,14 @@ namespace Reduce
 end Reduce
 
 -- https://plfa.github.io/DeBruijn/#values-do-not-reduce
-def Value.emptyReduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by
+def Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by
   introv v; is_empty; intro r
   cases v <;> try contradiction
-  · case succ v => cases r; · case succξ => apply (emptyReduce v).false; trivial
+  · case succ v => cases r; · case succξ => apply (empty_reduce v).false; trivial
 
-def Reduce.emptyValue : m —→ n → IsEmpty (Value m) := by
+def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by
   intro r; is_empty; intro v
-  have : ∀ {n}, IsEmpty (m —→ n) := Value.emptyReduce v
+  have : ∀ {n}, IsEmpty (m —→ n) := Value.empty_reduce v
   exact this.false r
 
 /--

Plfl/Lambda/Properties.lean

@@ -11,14 +11,14 @@ open Context Context.IsTy Term.Reduce
 open Sum
 
 -- https://plfa.github.io/Properties/#values-do-not-reduce
-def Value.emptyReduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by
+def Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by
   introv v; is_empty; intro r
   cases v <;> try contradiction
-  · case succ v => cases r; · case succξ => apply (emptyReduce v).false; trivial
+  · case succ v => cases r; · case succξ => apply (empty_reduce v).false; trivial
 
-def Reduce.emptyValue : m —→ n → IsEmpty (Value m) := by
+def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by
   intro r; is_empty; intro v
-  have : ∀ {n}, IsEmpty (m —→ n) := Value.emptyReduce v
+  have : ∀ {n}, IsEmpty (m —→ n) := Value.empty_reduce v
   exact this.false r
 
 -- https://plfa.github.io/Properties/#exercise-canonical--practice
@@ -113,7 +113,7 @@ def progress : ∅ ⊢ m ⦂ t → Progress m := Progress.ofIsTy
 -- https://plfa.github.io/Properties/#exercise-value-practice
 def IsTy.isValue : ∅ ⊢ m ⦂ t → Decidable (Nonempty (Value m)) := by
   intro j; cases progress j
-  · rename_i n r; have := Reduce.emptyValue r
+  · rename_i n r; have := Reduce.empty_value r
     apply isFalse; simp_all only [not_nonempty_iff]
   · exact isTrue ⟨by trivial⟩
 
@@ -396,24 +396,24 @@ def Reduce.det : (m —→ n) → (m —→ n') → n = n' := by
   intro r r'; cases r
   · case lamβ =>
     cases r' <;> try trivial
-    · case apξ₂ => exfalso; rename_i v _ _ r; exact (Value.emptyReduce v).false r
+    · case apξ₂ => exfalso; rename_i v _ _ r; exact (Value.empty_reduce v).false r
   · case apξ₁ =>
     cases r' <;> try trivial
     · case apξ₁ => simp only [Term.ap.injEq, and_true]; apply det <;> trivial
-    · case apξ₂ => exfalso; rename_i r _ v _; exact (Value.emptyReduce v).false r
+    · case apξ₂ => exfalso; rename_i r _ v _; exact (Value.empty_reduce v).false r
   · case apξ₂ =>
     cases r' <;> try trivial
-    · case lamβ => exfalso; rename_i r _ _ _ v; exact (Value.emptyReduce v).false r
-    · case apξ₁ => exfalso; rename_i v _ _ r; exact (Value.emptyReduce v).false r
+    · case lamβ => exfalso; rename_i r _ _ _ v; exact (Value.empty_reduce v).false r
+    · case apξ₁ => exfalso; rename_i v _ _ r; exact (Value.empty_reduce v).false r
     · case apξ₂ => simp only [Term.ap.injEq, true_and]; apply det <;> trivial
   · case zeroβ => cases r' <;> try trivial
   · case succβ =>
     cases r' <;> try trivial
-    · case caseξ => exfalso; rename_i v _ r; exact (Value.emptyReduce (Value.succ v)).false r
+    · case caseξ => exfalso; rename_i v _ r; exact (Value.empty_reduce (Value.succ v)).false r
   · case succξ => cases r'; · case succξ => simp only [Term.succ.injEq]; apply det <;> trivial
   · case caseξ =>
     cases r' <;> try trivial
-    · case succβ => exfalso; rename_i v r; exact (Value.emptyReduce (Value.succ v)).false r
+    · case succβ => exfalso; rename_i v r; exact (Value.empty_reduce (Value.succ v)).false r
     · case caseξ => simp only [Term.case.injEq, and_self, and_true]; apply det <;> trivial
   · case muβ => cases r'; try trivial
 

Plfl/More.lean

@@ -358,7 +358,7 @@ end Value
 /--
 `Reduce t t'` says that `t` reduces to `t'` via a given step.
 -/
-inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Type where
+inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Prop where
 | lamβ : Value v → Reduce ((ƛ n) □ v) (n ⇷ v)
 | apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m)
 | apξ₂ : Value v → Reduce m m' → Reduce (v □ m) (v □ m')
@@ -403,24 +403,17 @@ inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Type where
 | consβ : Reduce (.caseList (.cons v w) m n) (subst₂ v w n)
 
 -- https://plfa.github.io/DeBruijn/#reflexive-and-transitive-closure
-/--
-The predicate version of `Reduce`.
--/
-abbrev Reduce.ReduceP (t : Γ ⊢ a) (t' : Γ ⊢ a) := Nonempty (Reduce t t')
 
 namespace Notation
   scoped infix:40 " —→ " => Reduce
-  scoped infix:40 " —→ₚ " => Reduce.ReduceP
 end Notation
 
 namespace Reduce
-  instance : Coe (m —→ n) (m —→ₚ n) where coe r := ⟨r⟩
-
   /--
   A reflexive and transitive closure,
   defined as a sequence of zero or more steps of the underlying relation `—→`.
   -/
-  abbrev Clos {Γ a} := Relation.ReflTransGen (α := Γ ⊢ a) ReduceP
+  abbrev Clos {Γ a} := Relation.ReflTransGen (α := Γ ⊢ a) Reduce
 end Reduce
 
 namespace Notation
@@ -429,14 +422,14 @@ end Notation
 
 namespace Reduce.Clos
   abbrev refl : m —↠ m := .refl
-  abbrev tail : (m —↠ n) → (n —→ₚ n') → (m —↠ n') := .tail
-  abbrev head : (m —→ₚ n) → (n —↠ n') → (m —↠ n') := .head
-  abbrev single : (m —→ₚ n) → (m —↠ n) := .single
+  abbrev tail : (m —↠ n) → (n —→ n') → (m —↠ n') := .tail
+  abbrev head : (m —→ n) → (n —↠ n') → (m —↠ n') := .head
+  abbrev single : (m —→ n) → (m —↠ n) := .single
 
   instance : Coe (m —→ n) (m —↠ n) where coe r := .single r
 
   instance : Trans (α := Γ ⊢ a) Clos Reduce Clos where trans c r := c.tail r
-  instance : Trans (α := Γ ⊢ a) Reduce Reduce Clos where trans r r' := .tail r ⟨r'⟩
+  instance : Trans (α := Γ ⊢ a) Reduce Reduce Clos where trans r r' := .tail r r'
   instance : Trans (α := Γ ⊢ a) Reduce Clos Clos where trans r c := .head r c
 end Reduce.Clos
 
@@ -453,23 +446,21 @@ namespace Reduce
 end Reduce
 
 -- https://plfa.github.io/DeBruijn/#values-do-not-reduce
-def Value.emptyReduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by
-  introv v; is_empty; intro r
+def Value.not_reduce : Value m → ∀ {n}, ¬ m —→ n := by
+  introv v; intro r
   cases v with try contradiction
-  | succ v => cases r; · case succξ => apply (emptyReduce v).false; trivial
+  | succ v => cases r; · case succξ => apply not_reduce v; trivial
   | prod => cases r with
-    | prodξ₁ r => rename_i v _ _; apply (emptyReduce v).false; trivial
-    | prodξ₂ r => rename_i v _; apply (emptyReduce v).false; trivial
-  | left v => cases r; · case leftξ => apply (emptyReduce v).false; trivial
-  | right v => cases r; · case rightξ => apply (emptyReduce v).false; trivial
+    | prodξ₁ r => rename_i v _ _; apply not_reduce v; trivial
+    | prodξ₂ r => rename_i v _; apply not_reduce v; trivial
+  | left v => cases r; · case leftξ => apply not_reduce v; trivial
+  | right v => cases r; · case rightξ => apply not_reduce v; trivial
   | cons => cases r with
-    | consξ₁ r => rename_i v _ _; apply (emptyReduce v).false; trivial
-    | consξ₂ r => rename_i v _; apply (emptyReduce v).false; trivial
+    | consξ₁ r => rename_i v _ _; apply not_reduce v; trivial
+    | consξ₂ r => rename_i v _; apply not_reduce v; trivial
 
-def Reduce.emptyValue : m —→ n → IsEmpty (Value m) := by
-  intro r; is_empty; intro v
-  have : ∀ {n}, IsEmpty (m —→ n) := Value.emptyReduce v
-  exact this.false r
+def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by
+  intro r; is_empty; intro v; exact Value.not_reduce v r
 
 /--
 If a term `m` is not ill-typed, then it either is a value or can be reduced.

Plfl/More/Bisimulation.lean

@@ -7,35 +7,30 @@ open More
 open Subst Notation
 
 -- https://plfa.github.io/Bisimulation/#simulation
-inductive Sim : (Γ ⊢ a) → (Γ ⊢ a) → Type where
+inductive Sim : (Γ ⊢ a) → (Γ ⊢ a) → Prop where
 | var : Sim (` x)  (` x)
 | lam : Sim n n' → Sim (ƛ n) (ƛ n')
 | ap : Sim l l' → Sim m m' → Sim (l □ m) (l' □ m')
 | let : Sim l l' → Sim m m' → Sim (.let l m) (.let l' m')
-deriving BEq, DecidableEq, Repr
 
 namespace Sim
   scoped infix:40 " ~ " => Sim
 
-  noncomputable def refl_dec (t : Γ ⊢ a) : Decidable (Nonempty (t ~ t)) :=
-    open Classical (choice) in by
-      cases t with try (apply isFalse; intro ⟨s⟩; contradiction)
-      | var i => exact isTrue ⟨.var⟩
-      | lam t =>
-        if h : Nonempty (t ~ t) then
-          exact isTrue ⟨.lam <| choice h⟩
-        else
-          apply isFalse; intro ⟨.lam s⟩; exact h ⟨s⟩
-      | ap l m =>
-        if h : Nonempty (l ~ l) ∧ Nonempty (m ~ m) then
-          refine isTrue ⟨?_⟩; exact .ap (choice h.1) (choice h.2)
-        else
-          apply isFalse; intro ⟨.ap s s'⟩; exact h ⟨⟨s⟩, ⟨s'⟩⟩
-      | «let» m n =>
-        if h : Nonempty (m ~ m) ∧ Nonempty (n ~ n) then
-          refine isTrue ⟨?_⟩; exact .let (choice h.1) (choice h.2)
-        else
-          apply isFalse; intro ⟨.let s s'⟩; exact h ⟨⟨s⟩, ⟨s'⟩⟩
+  noncomputable def refl_dec (t : Γ ⊢ a) : Decidable (t ~ t) := by
+    cases t with try (apply isFalse; intro s; contradiction)
+    | var i => exact isTrue .var
+    | lam t =>
+      if h : t ~ t
+        then apply isTrue; exact .lam h
+        else apply isFalse; intro (.lam s); exact h s
+    | ap l m =>
+      if h : (l ~ l) ∧ (m ~ m)
+        then apply isTrue; exact .ap h.1 h.2
+        else apply isFalse; intro (.ap s s'); exact h ⟨s, s'⟩
+    | «let» m n =>
+      if h : (m ~ m) ∧ (n ~ n)
+        then apply isTrue; exact .let h.1 h.2
+        else apply isFalse; intro (.let s s'); exact h ⟨s, s'⟩
 
   -- https://plfa.github.io/Bisimulation/#exercise-_-practice
   def fromEq {s : (m : Γ ⊢ a) ~ m'} : (m' = n) → (m ~ n) := by
@@ -53,46 +48,47 @@ namespace Sim
       | «let» sm' sn' => simp only [toEq (s := sm') sm, toEq (s := sn') sn]
 
   -- https://plfa.github.io/Bisimulation/#simulation-commutes-with-values
-  def commValue {m m' : Γ ⊢ a} : (m ~ m') → Value m → Value m'
-  | .lam _, .lam => .lam
+  def commValue {m m' : Γ ⊢ a} : (m ~ m') → Value m → Value m' := by
+    intro s v; cases v with try contradiction
+    | lam => cases m' with try contradiction
+      | lam => exact .lam
 
   -- https://plfa.github.io/Bisimulation/#exercise-val¹-practice
-  def commValue_inv {m m' : Γ ⊢ a} : (m ~ m') → Value m' → Value m
-  | .lam _, .lam => .lam
+  def commValue_inv {m m' : Γ ⊢ a} : (m ~ m') → Value m' → Value m := by
+    intro s v; cases v with try contradiction
+    | lam => cases m with try contradiction
+      | lam => exact .lam
 
   -- https://plfa.github.io/Bisimulation/#simulation-commutes-with-renaming
   def commRename (ρ : ∀ {a}, Γ ∋ a → Δ ∋ a) {m m' : Γ ⊢ a}
   : m ~ m' → rename ρ m ~ rename ρ m'
-  := by
-    intro
-    | .var => exact .var
-    | .lam s => apply lam; exact commRename (ext ρ) s
-    | .ap sl sm => apply ap; repeat (apply commRename ρ; trivial)
-    | .let sl sm => apply «let»; repeat
-      first | apply commRename ρ | apply commRename (ext ρ)
-      trivial
+  := by intro
+  | .var => exact .var
+  | .lam s => apply lam; exact commRename (ext ρ) s
+  | .ap sl sm => apply ap; repeat (apply commRename ρ; trivial)
+  | .let sl sm => apply «let»; repeat
+    first | apply commRename ρ | apply commRename (ext ρ)
+    trivial
 
   -- https://plfa.github.io/Bisimulation/#simulation-commutes-with-substitution
   def commExts {σ σ' : ∀ {a}, Γ ∋ a → Δ ⊢ a}
   (gs : ∀ {a}, (x : Γ ∋ a) → σ x ~ σ' x)
   : (∀ {a b}, (x : Γ‚ b ∋ a) → exts σ x ~ exts σ' x)
-  := by
-    introv; match x with
-    | .z => simp only [exts]; exact .var
-    | .s x => simp only [exts]; apply commRename Lookup.s; apply gs
+  := by introv; match x with
+  | .z => simp only [exts]; exact .var
+  | .s x => simp only [exts]; apply commRename Lookup.s; apply gs
 
   def commSubst {σ σ' : ∀ {a}, Γ ∋ a → Δ ⊢ a}
   (gs : ∀ {a}, (x : Γ ∋ a) → @σ a x ~ @σ' a x)
   {m m' : Γ ⊢ a}
   : m ~ m' → subst σ m ~ subst σ' m'
-  := by
-    intro
-    | .var => apply gs
-    | .lam s => apply lam; exact commSubst (commExts gs) s
-    | .ap sl sm => apply ap; repeat (apply commSubst gs; trivial)
-    | .let sm sn => apply «let»; repeat
-      first | apply commSubst gs | apply commSubst (commExts gs)
-      trivial
+  := by intro
+  | .var => apply gs
+  | .lam s => apply lam; exact commSubst (commExts gs) s
+  | .ap sl sm => apply ap; repeat (apply commSubst gs; trivial)
+  | .let sm sn => apply «let»; repeat
+    first | apply commSubst gs | apply commSubst (commExts gs)
+    trivial
 
   def commSubst₁ {m m' : Γ ⊢ b} {n n' : Γ‚ b ⊢ a}
   (sm : m ~ m') (sn : n ~ n') : m ⇸ n ~ m' ⇸ n'

Plfl/Untyped/Denotational/Compositional.lean

@@ -114,7 +114,7 @@ inductive Holed : Context → Context → Type where
 | lam : Holed (Γ‚ ✶) (Δ‚ ✶) → Holed (Γ‚ ✶) Δ
 /-- Applying to a holed function makes a bigger hole. -/
 | apL : Holed Γ Δ → (Δ ⊢ ✶) → Holed Γ Δ
-/-- Applying a holed parameter makes a bigger hole. -/
+/-- Applying a holed argument makes a bigger hole. -/
 | apR : (Δ ⊢ ✶) → Holed Γ Δ → Holed Γ Δ
 
 /-- `plug`s a term into a `Holed` context, making a new term. -/