diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-05 16:16:42 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-05 16:16:42 +0000 |
| commit | a2bca9eb599e8109ba91e257ee223b39f64703c1 (patch) | |
| tree | 311f06f1a291c384434d2ec058f23c33f163eba3 | |
| parent | f2ad0f65cd73c834f0f94250141b2436c7edd63d (diff) | |
Remove incomplete unrolling proof.
| -rw-r--r-- | src/Cfe/Expression/Properties.agda | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda index 9af0d70..e810ce4 100644 --- a/src/Cfe/Expression/Properties.agda +++ b/src/Cfe/Expression/Properties.agda @@ -189,17 +189,6 @@ subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin insert′ x≈y xs≋ys F.zero = x≈y ∷ xs≋ys insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i -unroll : ∀ {n} → (e : Expression (suc n)) → μ e ≋ e [ μ e / F.zero ] -unroll e γ = begin - ⟦ μ e ⟧ γ ≈⟨ {!!} ⟩ - (λ X → ⟦ e ⟧ (X ∷ γ)) (⟦ μ e ⟧ γ) ≡⟨⟩ - ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ≡⟨⟩ - ⟦ e ⟧ (insert γ F.zero (⟦ μ e ⟧ γ)) ≈˘⟨ subst-fun e (μ e) F.zero γ ⟩ - ⟦ e [ μ e / F.zero ] ⟧ γ ∎ - where - open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) - open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE - monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_ monotone ⊥ γ≤γ′ = ≤-refl monotone ε γ≤γ′ = ≤-refl |