Prove alpha equivalence is reflexive.

1 files changed, 19 insertions, 2 deletions

diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda
index 80e104a..ecfbc92 100644
--- a/src/Data/Type/Properties.agda
+++ b/src/Data/Type/Properties.agda
@@ -15,12 +15,16 @@ open import Data.List.Membership.Propositional.Properties
 open import Data.List.Properties
 open import Data.List.Properties.Ext
 open import Data.List.Relation.Unary.Any using (Any)
-open import Data.Nat using (ℕ; _≟_; _+_)
+open import Data.Nat using (ℕ; _<_; _≟_; _+_)
+open import Data.Nat.Induction using (<-wellFounded)
+open import Data.Nat.Properties
 open import Data.Product using () renaming (_,_ to _,′_)
 open import Data.Sum as ⊎ using (_⊎_; fromInj₁; fromInj₂; [_,_])
 open import Data.Type mkFresh
-open import Function using (_⇔_; _∘_; _∘₂_; mk⇔; id; flip)
+open import Induction.WellFounded as Wf using (WfRec)
+open import Function using (_⇔_; _∘_; _∘₂_; _on_; mk⇔; id; flip)
 open import Relation.Binary hiding (_⇔_)
+import Relation.Binary.Construct.On as On using (wellFounded)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; sym; cong; cong₂; module ≡-Reasoning)
 open import Relation.Nullary using (Dec; Reflects; ¬_; _because_; yes; no)
@@ -229,3 +233,16 @@ free-≈ (all {α} {A} {β} {B} A≈B) = begin
           (P.subst (_∈ _) (sym β≡[β/α]x) x∈xs)
           (α≢x ∘ flip P.trans β≡[β/α]x))
     ... | yes α≡x = α≢x α≡x
+
+≈-refl : Reflexive _≈_
+≈-refl = Wf.All.wfRec (On.wellFounded size <-wellFounded) _ P go _
+  where
+  P : Type → Set
+  P A = A ≈ A
+
+  go : ∀ A → WfRec (_<_ on size) P A → P A
+  go (var α)     hyp = var α
+  go unit        hyp = unit
+  go (bin ⊗ A B) hyp = bin (hyp A (m≤m+n _ _)) (hyp B (m<n+m _ 0<1+n))
+  go (all α A)   hyp =
+    all (λ _ _ → hyp _ (P.subst (_< _) (sym (size-rename _ A)) (n<1+n _)))