module Orn.Reornament.Examples.Iterative (A B C : Set) where
open import Data.Unit
open import Data.Nat
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Level renaming (zero to zeroL ; suc to sucL)
open import Logic.Logic
open import Logic.IProp
open Logic.IProp.Applicative {zeroL}
open import IDesc.IDesc
open import IDesc.Fixpoint
open import Orn.Ornament
open import Orn.Reornament
test : func ⊤ ⊤
test = mk (λ x → `Σ A (λ a →
`Π B λ b →
`Σ Bool λ x →
`var tt))
forget : ℕ → ⊤
forget n = tt
testO : orn test forget forget
testO = mk (λ n → `Σ (λ a →
insert C (λ c →
`Π (λ b →
deleteΣ true
(`var (inv (ℕ.suc n)))))))
postulate
a : A
b : B
c : C
n : ℕ
x : Bool
xs : μ test tt
reorn1 : orn ⟦ testO ⟧orn proj₁ proj₁
reorn1 = ⌈ testO ⌉
reorn1O : Orn proj₁ (func.out ⟦ testO ⟧orn n)
reorn1O = orn.out reorn1 (n , ⟨ a , (λ _ → x , xs) ⟩)
reorn2 : orn ⟦ reorn1 ⟧orn proj₁ proj₁
reorn2 = ⌈ reorn1 ⌉
postulate
a' : A
xs⁺ : μ ⟦ testO ⟧orn (ℕ.suc n)
reorn2O : Orn proj₁ (func.out ⟦ reorn1 ⟧orn (n , ⟨ a , (λ _ → x , xs) ⟩))
reorn2O = orn.out reorn2 ((n , ⟨ a , (λ _ → x , xs) ⟩) , ⟨ a' , c , (λ _ → xs⁺) ⟩)
reorn3 : orn ⟦ reorn2 ⟧orn proj₁ proj₁
reorn3 = ⌈ reorn2 ⌉
postulate
c' : C
xs⁺⁺ : μ ⟦ reorn1 ⟧orn (ℕ.suc n , xs)
reorn3O : Orn proj₁ (func.out ⟦ reorn2 ⟧orn ((n , ⟨ a , (λ _ → true , xs) ⟩) , ⟨ (a , (c , (λ _ → xs⁺))) ⟩))
reorn3O = orn.out reorn3 (((n , ⟨ a , (λ _ → true , xs) ⟩) , ⟨ a , c , (λ _ → xs⁺) ⟩) , ⟨ (c' , (λ b → refl , xs⁺⁺)) ⟩)
lemma : ∀{i₁ i₂ i₃ i₄} → (x y : μ ⟦ reorn3 ⟧orn (((i₁ , i₂) , i₃) , i₄)) → ⊢ x ≡ y
lemma {i₂ = ⟨ i₂₁ , i₂₂ ⟩}
{⟨ .i₂₁ , i₄₁ , i₃₃ ⟩}
{⟨ .i₄₁ , i₄₂ ⟩}
⟨ refl , refl , x ⟩
⟨ refl , refl , y ⟩ = cong (λ x → ⟨ refl , refl , x ⟩) <$>
extensionality (λ b → lemma (x b) (y b))