From e0a703c0428946ff5ea70f02287d5d89adbd5a9f Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 7 Jul 2022 21:47:45 +0100 Subject: Prove alpha equivalence is reflexive. --- src/Data/Type/Properties.agda | 21 +++++++++++++++++++-- 1 file 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