text:
open import Nat
open import Prelude
open import List
open import contexts
open import unions

module core where
  -- types
  data typ : Set where
    _==>_ : typ → typ → typ
    ⟨⟩    : typ
    ⟨_×_⟩ : typ → typ → typ
    D[_]  : Nat → typ

  -- arrow type constructors bind very tightly
  infixr 25  _==>_

  -- type contexts, hole contexts, and datatype environments
  tctx = typ ctx
  hctx = (tctx ∧ typ) ctx
  denv = Σ[ dctx ∈ tctx ctx ]
    ∀{d1 d2 cctx1 cctx2 c} →
    d1 ≠ d2 →
    (d1 , cctx1) ∈ dctx →
    (d2 , cctx2) ∈ dctx →
    c # cctx1 ∨ c # cctx2

  -- simple values
  data val : Set where
    ⟨⟩    : val
    ⟨_,_⟩ : val → val → val
    C[_]_ : Nat → val → val

  -- examples
  data ex : Set where
    ⟨⟩    : ex
    ⟨_,_⟩ : ex → ex → ex
    C[_]_ : Nat → ex → ex
    _↦_  : val → ex → ex
    ¿¿    : ex

  -- simple value typing
  data _⊢_::ⱽ_ : denv → val → typ → Set where
    VTUnit : ∀{Σ'} → Σ' ⊢ ⟨⟩ ::ⱽ ⟨⟩
    VTPair : ∀{Σ' v1 v2 τ1 τ2} →
               Σ' ⊢ v1 ::ⱽ τ1 →
               Σ' ⊢ v2 ::ⱽ τ2 →
               Σ' ⊢ ⟨ v1 , v2 ⟩ ::ⱽ ⟨ τ1 × τ2 ⟩
    VTCtor : ∀{Σ' d cctx c v τ} →
               (d , cctx) ∈ π1 Σ' →
               (c , τ) ∈ cctx →
               Σ' ⊢ v ::ⱽ τ →
               Σ' ⊢ C[ c ] v ::ⱽ D[ d ]

  -- example typing
  data _,_⊢_:·_ : hctx → denv → ex → typ → Set where
    XTUnit  : ∀{Δ Σ'} → Δ , Σ' ⊢ ⟨⟩ :· ⟨⟩
    XTPair  : ∀{Δ Σ' ex1 ex2 τ1 τ2} →
                Δ , Σ' ⊢ ex1 :· τ1 →
                Δ , Σ' ⊢ ex2 :· τ2 →
                Δ , Σ' ⊢ ⟨ ex1 , ex2 ⟩ :· ⟨ τ1 × τ2 ⟩
    XTCtor  : ∀{Δ Σ' d cctx c ex τ} →
                (d , cctx) ∈ π1 Σ' →
                (c , τ) ∈ cctx →
                Δ , Σ' ⊢ ex :· τ →
                Δ , Σ' ⊢ C[ c ] ex :· D[ d ]
    XTTop   : ∀{Δ Σ' τ} → Δ , Σ' ⊢ ¿¿ :· τ
    XTInOut : ∀{Δ Σ' v ex τ1 τ2} →
                Σ' ⊢ v ::ⱽ τ1 →
                Δ , Σ' ⊢ ex :· τ2 →
                Δ , Σ' ⊢ v ↦ ex :· τ1 ==> τ2

  -- the two possible prj indices
  data prj-idx : Set where
    P1 : prj-idx
    P2 : prj-idx

  prj : {A : Set} → prj-idx → A → A → A
  prj P1 a1 a2 = a1
  prj P2 a1 a2 = a2

  mutual
    record rule : Set where
      inductive
      constructor |C_=>_
      field
        parm   : Nat
        branch : exp

    -- Expressions
    data exp : Set where
      fix_⦇·λ_=>_·⦈ : Nat → Nat → exp → exp
      _∘_           : exp → exp → exp
      X[_]          : Nat → exp
      ⟨⟩            : exp
      ⟨_,_⟩         : exp → exp → exp
      prj[_]_       : prj-idx → exp → exp
      C[_]_         : Nat → exp → exp
      case_of⦃·_·⦄ : exp → rule ctx → exp
      ??[_]         : Nat → exp
      PBE:assert    : exp → exp → exp

  -- u is fresh in e
  data hole-name-new : (e : exp) → (u : Nat) → Set where
    HNNFix  : ∀{x f e u} → hole-name-new e u → hole-name-new (fix f ⦇·λ x => e ·⦈) u
    HNNVar  : ∀{x u} → hole-name-new (X[ x ]) u
    HNNAp   : ∀{e1 e2 u} → hole-name-new e1 u → hole-name-new e2 u → hole-name-new (e1 ∘ e2) u
    HNNUnit : ∀{u} → hole-name-new ⟨⟩ u
    HNNPair : ∀{e1 e2 u} → hole-name-new e1 u → hole-name-new e2 u → hole-name-new ⟨ e1 , e2 ⟩ u
    HNNPrj  : ∀{e i u} → hole-name-new e u → hole-name-new (prj[ i ] e) u
    HNNCtor : ∀{c e u} → hole-name-new e u → hole-name-new (C[ c ] e) u
    HNNCase : ∀{e rules u} →
                hole-name-new e u →
                (∀{c rule} → (c , rule) ∈ rules → hole-name-new (rule.branch rule) u) →
                hole-name-new (case e of⦃· rules ·⦄) u
    HNNHole : ∀{u' u} → u' ≠ u → hole-name-new (??[ u' ]) u
    HNNAsrt : ∀{e1 e2 u} → hole-name-new e1 u → hole-name-new e2 u → hole-name-new (PBE:assert e1 e2) u

  -- e1 and e2 do not have any hole names in common
  data holes-disjoint : (e1 : exp) → (e2 : exp) → Set where
    HDFix  : ∀{x f e e'} → holes-disjoint e e' → holes-disjoint (fix f ⦇·λ x => e ·⦈) e'
    HDVar  : ∀{x e'} → holes-disjoint (X[ x ]) e'
    HDAp   : ∀{e1 e2 e'} → holes-disjoint e1 e' → holes-disjoint e2 e' → holes-disjoint (e1 ∘ e2) e'
    HDUnit : ∀{e'} → holes-disjoint ⟨⟩ e'
    HDPair : ∀{e1 e2 e'} → holes-disjoint e1 e' → holes-disjoint e2 e' → holes-disjoint ⟨ e1 , e2 ⟩ e'
    HDPrj  : ∀{i e e'} → holes-disjoint e e' → holes-disjoint (prj[ i ] e) e'
    HDCtor : ∀{c e e'} → holes-disjoint e e' → holes-disjoint (C[ c ] e) e'
    HDCase : ∀{e rules e'} →
               holes-disjoint e e' →
               (∀{c rule} → (c , rule) ∈ rules → holes-disjoint (rule.branch rule) e') →
               holes-disjoint (case e of⦃· rules ·⦄) e'
    HDHole : ∀{u e'} → hole-name-new e' u → holes-disjoint (??[ u ]) e'
    HDAsrt : ∀{e1 e2 e'} → holes-disjoint e1 e' → holes-disjoint e2 e' → holes-disjoint (PBE:assert e1 e2) e'

  -- e ecomplete iff e contains no holes
  data _ecomplete : exp → Set where
    ECFix  : ∀{f x e} → e ecomplete → fix f ⦇·λ x => e ·⦈ ecomplete
    ECVar  : ∀{x} → X[ x ] ecomplete
    ECAp   : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → (e1 ∘ e2) ecomplete
    ECUnit : ⟨⟩ ecomplete
    ECPair : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → ⟨ e1 , e2 ⟩ ecomplete
    ECPrj  : ∀{i e} → e ecomplete → (prj[ i ] e) ecomplete
    ECCtor : ∀{c e} → e ecomplete → (C[ c ] e) ecomplete
    ECCase : ∀{e rules} →
               e ecomplete →
               (∀{c rule} → (c , rule) ∈ rules → (rule.branch rule) ecomplete) →
               case e of⦃· rules ·⦄ ecomplete
    ECAsrt : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → (PBE:assert e1 e2) ecomplete

  -- type assignment for expressions
  data _,_,_⊢_::_ : hctx → denv → tctx → exp → typ → Set where
    TFix  : ∀{Δ Σ' Γ f x e τ1 τ2} →
              Δ , Σ' , (Γ ,, (f , τ1 ==> τ2) ,, (x , τ1)) ⊢ e :: τ2 →
              Δ , Σ' , Γ ⊢ fix f ⦇·λ x => e ·⦈ :: τ1 ==> τ2
    TVar  : ∀{Δ Σ' Γ x τ} → (x , τ) ∈ Γ → Δ , Σ' , Γ ⊢ X[ x ] :: τ
    THole : ∀{Δ Σ' Γ u τ} → (u , (Γ , τ)) ∈ Δ → Δ , Σ' , Γ ⊢ ??[ u ] :: τ
    TUnit : ∀{Δ Σ' Γ} → Δ , Σ' , Γ ⊢ ⟨⟩ :: ⟨⟩
    TPair : ∀{Δ Σ' Γ e1 e2 τ1 τ2} →
              holes-disjoint e1 e2 →
              Δ , Σ' , Γ ⊢ e1 :: τ1 →
              Δ , Σ' , Γ ⊢ e2 :: τ2 →
              Δ , Σ' , Γ ⊢ ⟨ e1 , e2 ⟩ :: ⟨ τ1 × τ2 ⟩
    TCtor : ∀{Δ Σ' Γ d cctx c e τ} →
              (d , cctx) ∈ π1 Σ' →
              (c , τ) ∈ cctx →
              Δ , Σ' , Γ ⊢ e :: τ →
              Δ , Σ' , Γ ⊢ C[ c ] e :: D[ d ]
    TApp  : ∀{Δ Σ' Γ f arg τ1 τ2} →
              holes-disjoint f arg →
              Δ , Σ' , Γ ⊢ f :: τ1 ==> τ2 →
              Δ , Σ' , Γ ⊢ arg :: τ1 →
              Δ , Σ' , Γ ⊢ f ∘ arg :: τ2
    TPrj  : ∀{Δ Σ' Γ i e τ1 τ2} →
              Δ , Σ' , Γ ⊢ e :: ⟨ τ1 × τ2 ⟩ →
              Δ , Σ' , Γ ⊢ prj[ i ] e :: prj i τ1 τ2
    TCase : ∀{Δ Σ' Γ d cctx e rules τ} →
              (d , cctx) ∈ π1 Σ' →
              Δ , Σ' , Γ ⊢ e :: D[ d ] →
              -- There must be a rule for each constructor, i.e. case exhuastiveness
              (∀{c} → dom cctx c → dom rules c) →
              (∀{c xc ec} →
                 (c , |C xc => ec) ∈ rules →
                   holes-disjoint ec e ∧
                   (∀{c' xc' ec'} → (c' , |C xc' => ec') ∈ rules → c ≠ c' → holes-disjoint ec ec') ∧
                   -- The constructor of each rule must be of the right datatype, and the branch must type-check
                   Σ[ τc ∈ typ ] (
                      (c , τc) ∈ cctx ∧
                      Δ , Σ' , (Γ ,, (xc , τc)) ⊢ ec :: τ)) →
              Δ , Σ' , Γ ⊢ case e of⦃· rules ·⦄ :: τ
    TAssert : ∀{Δ Σ' Γ e1 e2 τ} →
                holes-disjoint e1 e2 →
                Δ , Σ' , Γ ⊢ e1 :: τ →
                Δ , Σ' , Γ ⊢ e2 :: τ →
                Δ , Σ' , Γ ⊢ PBE:assert e1 e2 :: ⟨⟩

  mutual
    env : Set
    env = result ctx

    -- results - evaluation takes expressions to results, but results aren't necessarily final
    data result : Set where
      [_]fix_⦇·λ_=>_·⦈ : env → Nat → Nat → exp → result
      ⟨⟩               : result
      ⟨_,_⟩            : result → result → result
      C[_]_            : Nat → result → result
      [_]??[_]         : env → Nat → result
      _∘_              : result → result → result
      prj[_]_          : prj-idx → result → result
      [_]case_of⦃·_·⦄ : env → result → rule ctx → result
      C⁻¹[_]_           : Nat → result → result

  mutual
    data _env-final : env → Set where
      EFNone : ∅ env-final
      EFInd  : ∀{E x r} → E env-final → r final → (E ,, (x , r)) env-final

    -- final results are those that cannot be evaluated further
    data _final : result → Set where
      FDet   : ∀{r} → r det → r final
      FIndet : ∀{r} → r indet → r final

    -- final results that can be eliminated (or in the case of ⟨⟩, that don't need to be)
    data _det : result → Set where
      DFix  : ∀{E f x e} → E env-final → [ E ]fix f ⦇·λ x => e ·⦈ det
      DUnit : ⟨⟩ det
      DPair : ∀{r1 r2} → r1 final → r2 final → ⟨ r1 , r2 ⟩ det
      DCtor : ∀{c r} → r final → (C[ c ] r) det

    -- indeterminate results are incomplete and cannot be further reduced except by resumption
    data _indet : result → Set where
      IDHole : ∀{E u} → E env-final → [ E ]??[ u ] indet
      IDApp  : ∀{r1 r2} → r1 indet → r2 final → (r1 ∘ r2) indet
      IDPrj  : ∀{i r} → r indet → (prj[ i ] r) indet
      IDCase : ∀{E r rules} → E env-final → r indet → [ E ]case r of⦃· rules ·⦄ indet

  mutual
    -- type assignment for environments
    data _,_,_⊢_ : hctx → denv → tctx → env → Set where
      EnvId  : ∀{Δ Σ'} → Δ , Σ' , ∅ ⊢ ∅
      EnvInd : ∀{Δ Σ' Γ E x τx rx} →
                 Δ , Σ' , Γ ⊢ E →
                 Δ , Σ' ⊢ rx ·: τx →
                 Δ , Σ' , (Γ ,, (x , τx)) ⊢ (E ,, (x , rx))

    -- type assignment for results
    data _,_⊢_·:_ : hctx → denv → result → typ → Set where
      RTFix        : ∀{Δ Σ' Γ E f x e τ} →
                       Δ , Σ' , Γ ⊢ E →
                       Δ , Σ' , Γ ⊢ fix f ⦇·λ x => e ·⦈ :: τ →
                       Δ , Σ' ⊢ [ E ]fix f ⦇·λ x => e ·⦈ ·: τ
      RTHole       : ∀{Δ Σ' Γ E u τ} →
                       (u , (Γ , τ)) ∈ Δ →
                       Δ , Σ' , Γ ⊢ E →
                       Δ , Σ' ⊢ [ E ]??[ u ] ·: τ
      RTUnit       : ∀{Δ Σ'} → Δ , Σ' ⊢ ⟨⟩ ·: ⟨⟩
      RTPair       : ∀{Δ Σ' r1 r2 τ1 τ2} →
                       Δ , Σ' ⊢ r1 ·: τ1 →
                       Δ , Σ' ⊢ r2 ·: τ2 →
                       Δ , Σ' ⊢ ⟨ r1 , r2 ⟩ ·: ⟨ τ1 × τ2 ⟩
      RTCtor       : ∀{Δ Σ' d cctx c r τ} →
                       (d , cctx) ∈ π1 Σ' →
                       (c , τ) ∈ cctx →
                       Δ , Σ' ⊢ r ·: τ →
                       Δ , Σ' ⊢ C[ c ] r ·: D[ d ]
      RTApp        : ∀{Δ Σ' f arg τ1 τ2} →
                       Δ , Σ' ⊢ f ·: τ1 ==> τ2 →
                       Δ , Σ' ⊢ arg ·: τ1 →
                       Δ , Σ' ⊢ f ∘ arg ·: τ2
      RTPrj        : ∀{Δ Σ' i r τ1 τ2} →
                       Δ , Σ' ⊢ r ·: ⟨ τ1 × τ2 ⟩ →
                       Δ , Σ' ⊢ prj[ i ] r ·: prj i τ1 τ2
      RTCase       : ∀{Δ Σ' Γ E d cctx r rules τ} →
                       (d , cctx) ∈ π1 Σ' →
                       Δ , Σ' , Γ ⊢ E →
                       Δ , Σ' ⊢ r ·: D[ d ] →
                       -- There must be a rule for each constructor, i.e. case exhaustiveness
                       (∀{c} → dom cctx c → dom rules c) →
                       (∀{c xc ec} →
                          (c , |C xc => ec) ∈ rules →
                            -- The constructor of each rule must be of the right datatype, and the branch must type-check
                            Σ[ τc ∈ typ ] (
                               (c , τc) ∈ cctx ∧
                               Δ , Σ' , (Γ ,, (xc , τc)) ⊢ ec :: τ)) →
                       Δ , Σ' ⊢ [ E ]case r of⦃· rules ·⦄ ·: τ
      RTUnwrapCtor : ∀{Δ Σ' d cctx c r τ} →
                       (d , cctx) ∈ π1 Σ' →
                       (c , τ) ∈ cctx →
                       Δ , Σ' ⊢ r ·: D[ d ] →
                       Δ , Σ' ⊢ C⁻¹[ c ] r ·: τ

  excon         = env ∧ ex
  excons        = List excon
  assertions    = List (result ∧ val)
  hole-fillings = exp ctx
  constraints   = hole-fillings ∧ excons ctx

  record goal : Set where
    inductive
    constructor _⊢??[_]:_⊨_
    field
      g-tctx   : tctx
      g-id     : Nat
      g-typ    : typ
      g-excons : excons

  goals = List goal

  -- value-to-example coercion
  ⌊_⌋ : val → ex
  ⌊ ⟨⟩ ⌋ = ⟨⟩
  ⌊ ⟨ v1 , v2 ⟩ ⌋ = ⟨ ⌊ v1 ⌋ , ⌊ v2 ⌋ ⟩
  ⌊ C[ c ] v ⌋ = C[ c ] ⌊ v ⌋

  -- result-to-value coercion
  data ⌈_⌉:=_ : result → val → Set where
    CoerceUnit : ⌈ ⟨⟩ ⌉:= ⟨⟩
    CoercePair : ∀{r1 r2 v1 v2} →
                   ⌈ r1 ⌉:= v1 →
                   ⌈ r2 ⌉:= v2 →
                   ⌈ ⟨ r1 , r2 ⟩ ⌉:= ⟨ v1 , v2 ⟩
    CoerceCtor : ∀{c r v} →
                   ⌈ r ⌉:= v →
                   ⌈ C[ c ] r ⌉:= C[ c ] v

  -- excons typing
  data _,_⊢_::ˣ_,_ : hctx → denv → excons → tctx → typ → Set where
    TXNil : ∀{Δ Σ' Γ τ} → Δ , Σ' ⊢ [] ::ˣ Γ , τ
    TXInd : ∀{Δ Σ' X E ex Γ τ} →
              Δ , Σ' ⊢ X ::ˣ Γ , τ →
              Δ , Σ' , Γ ⊢ E →
              Δ , Σ' ⊢ ex :· τ →
              Δ , Σ' ⊢ ((E , ex) :: X) ::ˣ Γ , τ

  -- type assignment for hole fillings
  data _,_⊢ᴴ_ : hctx → denv → hole-fillings → Set where
    TFNil : ∀{Δ Σ'} → Δ , Σ' ⊢ᴴ ∅
    TFInd : ∀{Δ Σ' F u Γ τ e} →
              (u , Γ , τ) ∈ Δ →
              Δ , Σ' ⊢ᴴ F →
              Δ , Σ' , Γ ⊢ e :: τ →
              Δ , Σ' ⊢ᴴ (F ,, (u , e))

  {- TODO - we have to decide between this version and the one prior
  _,_⊢ₕ_ : hctx → denv → hole-fillings → Set
  Δ , Σ' ⊢ₕ F = ∀{u e} →
                  (u , e) ∈ F →
                  Σ[ Γ ∈ tctx ] Σ[ τ ∈ typ ] (
                     (u , Γ , τ) ∈ Δ ∧
                     Δ , Σ' , Γ ⊢ e :: τ)
  -}

  -- these are used to determine the "order" in which result consistency rules are checked
  not-both-pair : (r r' : result) → Set
  not-both-pair r r' = (∀{r1 r2} → r ≠ ⟨ r1 , r2 ⟩)  ∨ (∀{r1 r2} → r' ≠ ⟨ r1 , r2 ⟩)
  not-both-ctor : (r r' : result) → Set
  not-both-ctor r r' = (∀{c r''} → r ≠ (C[ c ] r'')) ∨ (∀{c r''} → r' ≠ (C[ c ] r''))

  -- result consistency
  data _≡⌊_⌋_ : result → assertions → result → Set where
    RCRefl    : ∀{r} → r ≡⌊ [] ⌋ r
    RCPair    : ∀{r1 r2 r'1 r'2 A1 A2} →
                  (_==_ {A = result} ⟨ r1 , r2 ⟩ ⟨ r'1 , r'2 ⟩ → ⊥) →
                  r1 ≡⌊ A1 ⌋ r'1 →
                  r2 ≡⌊ A2 ⌋ r'2 →
                  ⟨ r1 , r2 ⟩ ≡⌊ A1 ++ A2 ⌋ ⟨ r'1 , r'2 ⟩
    RCCtor    : ∀{c r r' A} →
                  (_==_ {A = result} (C[ c ] r) (C[ c ] r') → ⊥) →
                  r ≡⌊ A ⌋ r' →
                  (C[ c ] r) ≡⌊ A ⌋ (C[ c ] r')
    RCAssert1 : ∀{r1 r2 v2 A} →
                  r1 ≠ r2 →
                  not-both-pair r1 r2 →
                  not-both-ctor r1 r2 →
                  ⌈ r2 ⌉:= v2 →
                  A == (r1 , v2) :: [] →
                  r1 ≡⌊ A ⌋ r2
    RCAssert2 : ∀{r1 r2 v1 A} →
                  r1 ≠ r2 →
                  not-both-pair r1 r2 →
                  not-both-ctor r1 r2 →
                  ⌈ r1 ⌉:= v1 →
                  A == (r2 , v1) :: [] →
                  r1 ≡⌊ A ⌋ r2

  -- Generic result consistency failure - this goes through if results are not consistent
  data _≢_ : result → result → Set where
    RCFPair1    : ∀{r1 r2 r'1 r'2} →
                    r1 ≢ r'1 →
                    ⟨ r1 , r2 ⟩ ≢ ⟨ r'1 , r'2 ⟩
    RCFPair2    : ∀{r1 r2 r'1 r'2} →
                    r2 ≢ r'2 →
                    ⟨ r1 , r2 ⟩ ≢ ⟨ r'1 , r'2 ⟩
    RCFCtorMM   : ∀{c c' r r'} →
                    c ≠ c' →
                    (C[ c ] r) ≢ (C[ c' ] r')
    RCFCtor     : ∀{c r r'} →
                    r ≢ r' →
                    (C[ c ] r) ≢ (C[ c ] r')
    RCFNoCoerce : ∀{r r'} →
                    r ≠ r' →
                    not-both-pair r r' →
                    not-both-ctor r r' →
                    (∀{v} → ⌈ r  ⌉:= v → ⊥) →
                    (∀{v} → ⌈ r' ⌉:= v → ⊥) →
                    r ≢ r'

  -- Various judgments accept "fuel", which defines whether or not they can recurse indefinitely,
  -- and, if not, then the numerical limit. The limit is not on the recursion depth, but rather
  -- on the number of "beta reductions", interpreted a bit loosely to include case evaluations.
  -- - If ⌊ ⛽ ⌋ is ∞, then there is no beta reduction limit,
  --   but the judgment will not be satisfied unless evaluation eventually terminates.
  -- - If ⌊ ⛽ ⌋ is ⛽⟨ n ⟩, then the beta reduction limit is at most n,
  --   but if the limit is reached, then "success" judgments will not go through,
  --   but "failure" judgments will be satisfied automatically.
  data Fuel : Set where
    ∞ : Fuel
    ⛽⟨_⟩ : Nat → Fuel

  -- fuel depletion
  data _⛽⇓_ : Fuel → Fuel → Set where
    CF∞ : ∞ ⛽⇓ ∞
    CF⛽ : ∀{n} → ⛽⟨ 1+ n ⟩ ⛽⇓ ⛽⟨ n ⟩

  -- TODO we need a theorem that h-constraints cannot generate spurious hole names.
  -- generally, all the steps from an exp to an something with holes should not contain hole names
  -- not in the original exp, and the process as a whole should also not produce spurious names
  -- this realization probably means there are other important theorems that have been missed
  -- NOTE the core theorem in completeness.agda will do the trick for evaluation itself

  -- TODO we should have theorems that constrain where don't cares and such can be found.
  -- Don't cares should only be generated in backprop and should not appear anywhere else.

  -- Generic big step evaluation
  data _⊢_⌊_⌋⇒_⊣_ : env → exp → Fuel → result → assertions → Set where
    EUnit       : ∀{E ⛽} → E ⊢ ⟨⟩ ⌊ ⛽ ⌋⇒ ⟨⟩ ⊣ []
    EPair       : ∀{E ⛽ e1 e2 r1 r2 A1 A2} →
                    E ⊢ e1 ⌊ ⛽ ⌋⇒ r1 ⊣ A1 →
                    E ⊢ e2 ⌊ ⛽ ⌋⇒ r2 ⊣ A2 →
                    E ⊢ ⟨ e1 , e2 ⟩ ⌊ ⛽ ⌋⇒ ⟨ r1 , r2 ⟩ ⊣ A1 ++ A2
    ECtor       : ∀{E ⛽ c e r A} →
                    E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
                    E ⊢ C[ c ] e ⌊ ⛽ ⌋⇒ (C[ c ] r) ⊣ A
    EFix        : ∀{E ⛽ f x e} → E ⊢ fix f ⦇·λ x => e ·⦈ ⌊ ⛽ ⌋⇒ [ E ]fix f ⦇·λ x => e ·⦈ ⊣ []
    EVar        : ∀{E ⛽ x r} → (x , r) ∈ E → E ⊢ X[ x ] ⌊ ⛽ ⌋⇒ r ⊣ []
    EHole       : ∀{E ⛽ u} → E ⊢ ??[ u ] ⌊ ⛽ ⌋⇒ [ E ]??[ u ] ⊣ []
    EAppFix     : ∀{E ⛽ ⛽↓ e1 e2 Ef f x ef r1 A1 r2 A2 r A} →
                    ⛽ ⛽⇓ ⛽↓ →
                    E ⊢ e1 ⌊ ⛽ ⌋⇒ r1 ⊣ A1 →
                    r1 == [ Ef ]fix f ⦇·λ x => ef ·⦈ →
                    E ⊢ e2 ⌊ ⛽ ⌋⇒ r2 ⊣ A2 →
                    (Ef ,, (f , r1) ,, (x , r2)) ⊢ ef ⌊ ⛽↓ ⌋⇒ r ⊣ A →
                    E ⊢ e1 ∘ e2 ⌊ ⛽ ⌋⇒ r ⊣ A1 ++ A2 ++ A
    EAppIndet   : ∀{E ⛽ e1 e2 r1 A1 r2 A2} →
                    E ⊢ e1 ⌊ ⛽ ⌋⇒ r1 ⊣ A1 →
                    (∀{Ef f x ef} → r1 ≠ [ Ef ]fix f ⦇·λ x => ef ·⦈) →
                    E ⊢ e2 ⌊ ⛽ ⌋⇒ r2 ⊣ A2 →
                    E ⊢ e1 ∘ e2 ⌊ ⛽ ⌋⇒ (r1 ∘ r2) ⊣ A1 ++ A2
    EPrj        : ∀{E ⛽ i e r1 r2 A} →
                    E ⊢ e ⌊ ⛽ ⌋⇒ ⟨ r1 , r2 ⟩ ⊣ A →
                    E ⊢ prj[ i ] e ⌊ ⛽ ⌋⇒ prj i r1 r2 ⊣ A
    EPrjIndet   : ∀{E ⛽ i e r A} →
                    E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
                    (∀{r1 r2} → r ≠ ⟨ r1 , r2 ⟩) →
                    E ⊢ prj[ i ] e ⌊ ⛽ ⌋⇒ prj[ i ] r ⊣ A
    ECase       : ∀{E ⛽ ⛽↓ e rules c xc ec r A' rc A} →
                    ⛽ ⛽⇓ ⛽↓ →
                    (c , |C xc => ec) ∈ rules →
                    E ⊢ e ⌊ ⛽ ⌋⇒ (C[ c ] r) ⊣ A →
                    (E ,, (xc , r)) ⊢ ec ⌊ ⛽↓ ⌋⇒ rc ⊣ A' →
                    E ⊢ case e of⦃· rules ·⦄ ⌊ ⛽ ⌋⇒ rc ⊣ A ++ A'
    ECaseIndet  : ∀{E ⛽ e rules r A} →
                    E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
                    (∀{c rc} → r ≠ (C[ c ] rc)) →
                    E ⊢ case e of⦃· rules ·⦄ ⌊ ⛽ ⌋⇒ [ E ]case r of⦃· rules ·⦄ ⊣ A
    EAssert     : ∀{E ⛽ e1 r1 A1 e2 r2 A2 A3} →
                    E ⊢ e1 ⌊ ⛽ ⌋⇒ r1 ⊣ A1 →
                    E ⊢ e2 ⌊ ⛽ ⌋⇒ r2 ⊣ A2 →
                    r1 ≡⌊ A3 ⌋ r2 →
                    E ⊢ PBE:assert e1 e2 ⌊ ⛽ ⌋⇒ ⟨⟩ ⊣ A1 ++ A2 ++ A3

  -- Generic evaluation failure - this goes through if evaluation would fail due to failure
  -- of some assertion that occurs during evaluation, or if the fuel runs out.
  data _⊢_⌊_⌋⇒∅ : env → exp → Fuel → Set where
    EFPair1      : ∀{E ⛽ e1 e2} →
                     E ⊢ e1 ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ ⟨ e1 , e2 ⟩ ⌊ ⛽ ⌋⇒∅
    EFPair2      : ∀{E ⛽ e1 e2} →
                     E ⊢ e2 ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ ⟨ e1 , e2 ⟩ ⌊ ⛽ ⌋⇒∅
    EFCtor       : ∀{E ⛽ c e} →
                     E ⊢ e ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ C[ c ] e ⌊ ⛽ ⌋⇒∅
    EFAppFun     : ∀{E ⛽ e1 e2} →
                     E ⊢ e1 ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ e1 ∘ e2 ⌊ ⛽ ⌋⇒∅
    EFAppArg     : ∀{E ⛽ e1 e2} →
                     E ⊢ e2 ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ e1 ∘ e2 ⌊ ⛽ ⌋⇒∅
    EFAppEval    : ∀{E ⛽ ⛽↓ e1 e2 Ef f x ef r1 A1 r2 A2} →
                     ⛽ ⛽⇓ ⛽↓ →
                     E ⊢ e1 ⌊ ⛽ ⌋⇒ r1 ⊣ A1 →
                     r1 == [ Ef ]fix f ⦇·λ x => ef ·⦈ →
                     E ⊢ e2 ⌊ ⛽ ⌋⇒ r2 ⊣ A2 →
                     (Ef ,, (f , r1) ,, (x , r2)) ⊢ ef ⌊ ⛽↓ ⌋⇒∅ →
                     E ⊢ e1 ∘ e2 ⌊ ⛽ ⌋⇒∅
    EFPrj        : ∀{E ⛽ i e} →
                     E ⊢ e ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ prj[ i ] e ⌊ ⛽ ⌋⇒∅
    EFCaseScrut  : ∀{E ⛽ e rules} →
                     E ⊢ e ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ case e of⦃· rules ·⦄ ⌊ ⛽ ⌋⇒∅
    EFCaseRule   : ∀{E ⛽ ⛽↓ e rules c xc ec r A} →
                     ⛽ ⛽⇓ ⛽↓ →
                     (c , |C xc => ec) ∈ rules →
                     E ⊢ e ⌊ ⛽ ⌋⇒ (C[ c ] r) ⊣ A →
                     (E ,, (xc , r)) ⊢ ec ⌊ ⛽↓ ⌋⇒∅ →
                     E ⊢ case e of⦃· rules ·⦄ ⌊ ⛽ ⌋⇒∅
    EFAssert1    : ∀{E ⛽ e1 e2} →
                     E ⊢ e1 ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ PBE:assert e1 e2 ⌊ ⛽ ⌋⇒∅
    EFAssert2    : ∀{E ⛽ e1 e2} →
                     E ⊢ e2 ⌊ ⛽ ⌋⇒∅ →
                     E ⊢ PBE:assert e1 e2 ⌊ ⛽ ⌋⇒∅
    EFAssert     : ∀{E ⛽ e1 r1 A1 e2 r2 A2} →
                     E ⊢ e1 ⌊ ⛽ ⌋⇒ r1 ⊣ A1 →
                     E ⊢ e2 ⌊ ⛽ ⌋⇒ r2 ⊣ A2 →
                     r1 ≢ r2 →
                     E ⊢ PBE:assert e1 e2 ⌊ ⛽ ⌋⇒∅
    EFLimit      : ∀{E e} → E ⊢ e ⌊ ⛽⟨ 0 ⟩ ⌋⇒∅

  -- resumption
  mutual
    data _⊢_⌊_⌋:⇨_:=_ : hole-fillings → env → Fuel → env → assertions → Set where
      RENil : ∀{⛽ F} → F ⊢ ∅ ⌊ ⛽ ⌋:⇨ ∅ := []
      REInd : ∀{⛽ F E E' x r r' A A'} →
                F ⊢ E ⌊ ⛽ ⌋:⇨ E' := A →
                F ⊢ r ⌊ ⛽ ⌋⇨ r' := A' →
                F ⊢ E ,, (x , r) ⌊ ⛽ ⌋:⇨ (E' ,, (x , r')) := A ++ A'

    data _⊢_⌊_⌋⇨_:=_ : hole-fillings → result → Fuel → result → assertions → Set where
      RHoleResume  : ∀{⛽ F E u r r' e A A'} →
                       (u , e) ∈ F →
                       E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
                       F ⊢ r ⌊ ⛽ ⌋⇨ r' := A' →
                       F ⊢ [ E ]??[ u ] ⌊ ⛽ ⌋⇨ r' := A ++ A'
      RHoleIndet   : ∀{⛽ F E E' u A} →
                       u # F →
                       F ⊢ E ⌊ ⛽ ⌋:⇨ E' := A →
                       F ⊢ [ E ]??[ u ] ⌊ ⛽ ⌋⇨ [ E' ]??[ u ] := A
      RUnit        : ∀{⛽ F} → F ⊢ ⟨⟩ ⌊ ⛽ ⌋⇨ ⟨⟩ := []
      RPair        : ∀{⛽ F r1 r2 r1' r2' A1 A2} →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨ r1' := A1 →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨ r2' := A2 →
                       F ⊢ ⟨ r1 , r2 ⟩ ⌊ ⛽ ⌋⇨ ⟨ r1' , r2' ⟩ := A1 ++ A2
      RCtor        : ∀{⛽ F c r r' A} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ r' := A →
                       F ⊢ C[ c ] r ⌊ ⛽ ⌋⇨ (C[ c ] r') := A
      RApp         : ∀{⛽ ⛽↓ F r1 r2 r r' Ef f x ef r1' r2' A1 A2 Af A'} →
                       ⛽ ⛽⇓ ⛽↓ →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨ r1' := A1 →
                       r1' == [ Ef ]fix f ⦇·λ x => ef ·⦈ →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨ r2' := A2 →
                       (Ef ,, (f , r1') ,, (x , r2')) ⊢ ef ⌊ ⛽↓ ⌋⇒ r ⊣ Af →
                       F ⊢ r ⌊ ⛽↓ ⌋⇨ r' := A' →
                       F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨ r' := A1 ++ A2 ++ Af ++ A'
      RAppIndet    : ∀{⛽ F r1 r2 r1' r2' A1 A2} →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨ r1' := A1 →
                       (∀{Ef f x ef} → r1' ≠ [ Ef ]fix f ⦇·λ x => ef ·⦈) →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨ r2' := A2 →
                       F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨ (r1' ∘ r2') := A1 ++ A2
      RFix         : ∀{⛽ F E E' f x e A} →
                       F ⊢ E ⌊ ⛽ ⌋:⇨ E' := A →
                       F ⊢ [ E ]fix f ⦇·λ x => e ·⦈ ⌊ ⛽ ⌋⇨ [ E' ]fix f ⦇·λ x => e ·⦈ := A
      RPrj         : ∀{⛽ F i r r1 r2 A} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ ⟨ r1 , r2 ⟩ := A →
                       F ⊢ prj[ i ] r ⌊ ⛽ ⌋⇨ prj i r1 r2 := A
      RPrjIndet    : ∀{⛽ F i r r' A} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ r' := A →
                       (∀{r1 r2} → r' ≠ ⟨ r1 , r2 ⟩) →
                       F ⊢ prj[ i ] r ⌊ ⛽ ⌋⇨ prj[ i ] r' := A
      RCase        : ∀{⛽ F E r rules c xc ec r' rc A A'} →
                       (c , |C xc => ec) ∈ rules →
                       F ⊢ r ⌊ ⛽ ⌋⇨ (C[ c ] r') := A →
                       F ⊢ [ E ]fix xc ⦇·λ xc => ec ·⦈ ∘ (C⁻¹[ c ] r) ⌊ ⛽ ⌋⇨ rc := A' →
                       F ⊢ [ E ]case r of⦃· rules ·⦄ ⌊ ⛽ ⌋⇨ rc := A ++ A'
      RCaseIndet   : ∀{⛽ F E E' r rules r' A A'} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ r' := A →
                       (∀{c rc} → r' ≠ (C[ c ] rc)) →
                       F ⊢ E ⌊ ⛽ ⌋:⇨ E' := A' →
                       F ⊢ [ E ]case r of⦃· rules ·⦄ ⌊ ⛽ ⌋⇨ [ E' ]case r' of⦃· rules ·⦄ := A ++ A'
      RUnwrapCtor  : ∀{⛽ F r c rc A} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ C[ c ] rc := A →
                       F ⊢ C⁻¹[ c ] r ⌊ ⛽ ⌋⇨ rc := A
      RUnwrapIndet : ∀{⛽ F c r r' A} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ r' := A →
                       (∀{rc} → r' ≠ (C[ c ] rc)) →
                       F ⊢ C⁻¹[ c ] r ⌊ ⛽ ⌋⇨ C⁻¹[ c ] r' := A

  -- Generic resumption failure - this goes through if resumption would fail due to failure
  -- of some evaluation that occurs during resumption.
  mutual
    data _⊢_⌊_⌋:⇨∅ : hole-fillings → env → Fuel → Set where
      RFERes : ∀{⛽ F E x r} →
                 F ⊢ r ⌊ ⛽ ⌋⇨∅ →
                 F ⊢ (E ,, (x , r)) ⌊ ⛽ ⌋:⇨∅
      RFEEnv : ∀{⛽ F E x r} →
                 F ⊢ E ⌊ ⛽ ⌋:⇨∅ →
                 F ⊢ (E ,, (x , r)) ⌊ ⛽ ⌋:⇨∅

      {- TODO we must choose between this approach and the one prior
      RFE : ∀{⛽ F E x r} →
              (x , r) ∈ E →
              F ⊢ r ⌊ ⛽ ⌋⇨∅ →
              F ⊢ E ⌊ ⛽ ⌋:⇨∅
      -}

    data _⊢_⌊_⌋⇨∅ : hole-fillings → result → Fuel → Set where
      RFHoleEval   : ∀{⛽ F E u e} →
                       (u , e) ∈ F →
                       E ⊢ e ⌊ ⛽ ⌋⇒∅ →
                       F ⊢ [ E ]??[ u ] ⌊ ⛽ ⌋⇨∅
      RFHoleRes    : ∀{⛽ F E u e r A} →
                       (u , e) ∈ F →
                       E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
                       F ⊢ r ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ [ E ]??[ u ] ⌊ ⛽ ⌋⇨∅
      RFHoleIndet  : ∀{⛽ F E u} →
                       u # F →
                       F ⊢ E ⌊ ⛽ ⌋:⇨∅ →
                       F ⊢ [ E ]??[ u ] ⌊ ⛽ ⌋⇨∅
      RFPair1      : ∀{⛽ F r1 r2} →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ ⟨ r1 , r2 ⟩ ⌊ ⛽ ⌋⇨∅
      RFPair2      : ∀{⛽ F r1 r2} →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ ⟨ r1 , r2 ⟩ ⌊ ⛽ ⌋⇨∅
      RFCtor       : ∀{⛽ F c r} →
                       F ⊢ r ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ C[ c ] r ⌊ ⛽ ⌋⇨∅
      RFAppFun     : ∀{⛽ F r1 r2} →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨∅
      RFAppArg     : ∀{⛽ F r1 r2} →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨∅
      RFAppEval    : ∀{⛽ ⛽↓ F r1 r2 Ef f x ef r1' r2' A1 A2} →
                       ⛽ ⛽⇓ ⛽↓ →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨ r1' := A1 →
                       r1' == [ Ef ]fix f ⦇·λ x => ef ·⦈ →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨ r2' := A2 →
                       (Ef ,, (f , r1') ,, (x , r2')) ⊢ ef ⌊ ⛽↓ ⌋⇒∅ →
                       F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨∅
      RFAppRes     : ∀{⛽ ⛽↓ F r1 r2 Ef f x ef r1' r2' r A1 A2 Af} →
                       ⛽ ⛽⇓ ⛽↓ →
                       F ⊢ r1 ⌊ ⛽ ⌋⇨ r1' := A1 →
                       r1' == [ Ef ]fix f ⦇·λ x => ef ·⦈ →
                       F ⊢ r2 ⌊ ⛽ ⌋⇨ r2' := A2 →
                       (Ef ,, (f , r1') ,, (x , r2')) ⊢ ef ⌊ ⛽↓ ⌋⇒ r ⊣ Af →
                       F ⊢ r ⌊ ⛽↓ ⌋⇨∅ →
                       F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨∅
      RFFix        : ∀{⛽ F E f x e} →
                       F ⊢ E ⌊ ⛽ ⌋:⇨∅ →
                       F ⊢ [ E ]fix f ⦇·λ x => e ·⦈ ⌊ ⛽ ⌋⇨∅
      RFPrj        : ∀{⛽ F i r} →
                       F ⊢ r ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ prj[ i ] r ⌊ ⛽ ⌋⇨∅
      RFCaseScrut  : ∀{⛽ F E r rules} →
                       F ⊢ r ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ [ E ]case r of⦃· rules ·⦄ ⌊ ⛽ ⌋⇨∅
      RFCase       : ∀{⛽ F E r rules c xc ec r' A} →
                       (c , |C xc => ec) ∈ rules →
                       F ⊢ r ⌊ ⛽ ⌋⇨ (C[ c ] r') := A →
                       F ⊢ [ E ]fix xc ⦇·λ xc => ec ·⦈ ∘ (C⁻¹[ c ] r) ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ [ E ]case r of⦃· rules ·⦄ ⌊ ⛽ ⌋⇨∅
      RFCaseIndet  : ∀{⛽ F E r rules r' A} →
                       F ⊢ r ⌊ ⛽ ⌋⇨ r' := A →
                       (∀{c rc} → r' ≠ (C[ c ] rc)) →
                       F ⊢ E ⌊ ⛽ ⌋:⇨∅ →
                       F ⊢ [ E ]case r of⦃· rules ·⦄ ⌊ ⛽ ⌋⇨∅
      RFUnwrapCtor : ∀{⛽ F c r} →
                       F ⊢ r ⌊ ⛽ ⌋⇨∅ →
                       F ⊢ C⁻¹[ c ] r ⌊ ⛽ ⌋⇨∅
      RFLimit      : ∀{F r} → F ⊢ r ⌊ ⛽⟨ 0 ⟩ ⌋⇨∅

  data Filter_:=_ : excons → excons → Set where
    FilterNil : Filter [] := []
    FilterYes : ∀{X X' E ex} →
                  Filter X := X' →
                  ex ≠ ¿¿ →
                  Filter (E , ex) :: X := ((E , ex) :: X')
    FilterNo  : ∀{X X' E} →
                  Filter X := X' →
                  Filter (E , ¿¿) :: X := X'

  -- Assertion Satisfaction and Simplification
  data _⌊_⌋⊨ᴬ_ : hole-fillings → Fuel → assertions → Set where
    SANil : ∀{⛽ F} → F ⌊ ⛽ ⌋⊨ᴬ []
    SAInd : ∀{⛽ F r v r' A A'} →
              F ⌊ ⛽ ⌋⊨ᴬ A →
              F ⊢ r ⌊ ⛽ ⌋⇨ r' := A' →
              F ⌊ ⛽ ⌋⊨ᴬ A' →
              ⌈ r' ⌉:= v →
              F ⌊ ⛽ ⌋⊨ᴬ ((r , v) :: A)

  -- Example Satisfaction (of Results)
  data _⊢_⌊_⌋⊨ᴿ_ : hole-fillings → result → Fuel → ex → Set where
    XSTop   : ∀{⛽ F r} → F ⊢ r ⌊ ⛽ ⌋⊨ᴿ ¿¿
    XSUnit  : ∀{⛽ F} → F ⊢ ⟨⟩ ⌊ ⛽ ⌋⊨ᴿ ⟨⟩
    XSPair  : ∀{⛽ F r1 r2 ex1 ex2} →
                F ⊢ r1 ⌊ ⛽ ⌋⊨ᴿ ex1 →
                F ⊢ r2 ⌊ ⛽ ⌋⊨ᴿ ex2 →
                F ⊢ ⟨ r1 , r2 ⟩ ⌊ ⛽ ⌋⊨ᴿ ⟨ ex1 , ex2 ⟩
    XSCtor  : ∀{⛽ F r c ex} →
                F ⊢ r ⌊ ⛽ ⌋⊨ᴿ ex →
                F ⊢ C[ c ] r ⌊ ⛽ ⌋⊨ᴿ (C[ c ] ex)
    XSInOut : ∀{⛽ F r1 r2 v2 ex r A} →
                ⌈ r2 ⌉:= v2 →
                F ⊢ r1 ∘ r2 ⌊ ⛽ ⌋⇨ r := A →
                F ⊢ r ⌊ ⛽ ⌋⊨ᴿ ex →
                F ⌊ ⛽ ⌋⊨ᴬ A →
                F ⊢ r1 ⌊ ⛽ ⌋⊨ᴿ (v2 ↦ ex)

  -- Example Satisfaction (of Expressions)
  data _⊢_⌊_⌋⊨ᴱ_ : hole-fillings → exp → Fuel → excons → Set where
    SatNil : ∀{⛽ F e} → F ⊢ e ⌊ ⛽ ⌋⊨ᴱ []
    SatTop : ∀{⛽ F e E X} →
               F ⊢ e ⌊ ⛽ ⌋⊨ᴱ X →
               F ⊢ e ⌊ ⛽ ⌋⊨ᴱ ((E , ¿¿) :: X)
    SatInd : ∀{⛽ F e E ex X r r' A A'} →
               ex ≠ ¿¿ →
               F ⊢ e ⌊ ⛽ ⌋⊨ᴱ X →
               E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
               F ⊢ r ⌊ ⛽ ⌋⇨ r' := A' →
               F ⊢ r' ⌊ ⛽ ⌋⊨ᴿ ex →
               F ⌊ ⛽ ⌋⊨ᴬ A ++ A' →
               F ⊢ e ⌊ ⛽ ⌋⊨ᴱ ((E , ex) :: X)

  data _⌊_⌋⊨ᵁ_ : hole-fillings → Fuel → excons ctx → Set where
    CSNil : ∀{⛽ F} → F ⌊ ⛽ ⌋⊨ᵁ ∅
    CSInd : ∀{⛽ F U u X} →
              F ⌊ ⛽ ⌋⊨ᵁ U →
              F ⊢ ??[ u ] ⌊ ⛽ ⌋⊨ᴱ X →
              F ⌊ ⛽ ⌋⊨ᵁ (U ,, (u , X))

  -- Constraint Satisfaction
  _⌊_⌋⊨ᴷ_ : hole-fillings → Fuel → constraints → Set
  F ⌊ ⛽ ⌋⊨ᴷ (F0 , U) =
    (∀{u e} → (u , e) ∈ F0 → (u , e) ∈ F) ∧
    F ⌊ ⛽ ⌋⊨ᵁ U

  -- constraints merge
  _⊕_:=_ : constraints → constraints → constraints → Set
  (F1 , U1) ⊕ (F2 , U2) := (F' , U') = F1 ≈ F2 ∧ F1 ∪ F2 == F' ∧ U1 ⊎ U2 == U'

  mutual
    -- example unevaluation
    data _,_,_⊢_⇐⌊_⌋_:=_ : hctx → denv → hole-fillings → result → Fuel → ex → constraints → Set where
      UTop        : ∀{⛽ Δ Σ' F r} → Δ , Σ' , F ⊢ r ⇐⌊ ⛽ ⌋ ¿¿ := (∅ , ∅)
      UHole       : ∀{⛽ Δ Σ' F E u ex} →
                      ex ≠ ¿¿ →
                      Δ , Σ' , F ⊢ [ E ]??[ u ] ⇐⌊ ⛽ ⌋ ex := (∅ , ■ (u , (E , ex) :: []))
      UUnit       : ∀{⛽ Δ Σ' F} → Δ , Σ' , F ⊢ ⟨⟩ ⇐⌊ ⛽ ⌋ ⟨⟩ := (∅ , ∅)
      UCtor       : ∀{⛽ Δ Σ' F c r ex K} →
                      Δ , Σ' , F ⊢ r ⇐⌊ ⛽ ⌋ ex := K →
                      Δ , Σ' , F ⊢ C[ c ] r ⇐⌊ ⛽ ⌋ C[ c ] ex := K
      UPair       : ∀{⛽ Δ Σ' F r1 r2 ex1 ex2 K1 K2 K'} →
                      Δ , Σ' , F ⊢ r1 ⇐⌊ ⛽ ⌋ ex1 := K1 →
                      Δ , Σ' , F ⊢ r2 ⇐⌊ ⛽ ⌋ ex2 := K2 →
                      K1 ⊕ K2 := K' →
                      Δ , Σ' , F ⊢ ⟨ r1 , r2 ⟩ ⇐⌊ ⛽ ⌋ ⟨ ex1 , ex2 ⟩ := K'
      UFix        : ∀{⛽ ⛽↓ Δ Σ' F E f x e rf v r ex K} →
                      ⛽ ⛽⇓ ⛽↓ →
                      rf == [ E ]fix f ⦇·λ x => e ·⦈ →
                      ⌈ r ⌉:= v →
                      Δ , Σ' , F ⊢ e ⌊ ⛽ ⌋⇌ ((E ,, (f , rf) ,, (x , r)) , ex) :: [] := K →
                      Δ , Σ' , F ⊢ rf ⇐⌊ ⛽ ⌋ v ↦ ex := K
      UApp        : ∀{⛽ Δ Σ' F r1 r2 ex v2 K} →
                      ex ≠ ¿¿ →
                      ⌈ r2 ⌉:= v2 →
                      Δ , Σ' , F ⊢ r1 ⇐⌊ ⛽ ⌋ v2 ↦ ex := K →
                      Δ , Σ' , F ⊢ r1 ∘ r2 ⇐⌊ ⛽ ⌋ ex := K
      UPrj1       : ∀{⛽ Δ Σ' F r ex K} →
                      ex ≠ ¿¿ →
                      Δ , Σ' , F ⊢ r ⇐⌊ ⛽ ⌋ ⟨ ex , ¿¿ ⟩ := K →
                      Δ , Σ' , F ⊢ prj[ P1 ] r ⇐⌊ ⛽ ⌋ ex := K
      UPrj2       : ∀{⛽ Δ Σ' F r ex K} →
                      ex ≠ ¿¿ →
                      Δ , Σ' , F ⊢ r ⇐⌊ ⛽ ⌋ ⟨ ¿¿ , ex ⟩ := K →
                      Δ , Σ' , F ⊢ prj[ P2 ] r ⇐⌊ ⛽ ⌋ ex := K
      UCase       : ∀{⛽ ⛽↓ Δ Σ' F E r rules ex c xc ec K1 K2 K'} →
                      ex ≠ ¿¿ →
                      ⛽ ⛽⇓ ⛽↓ →
                      (c , |C xc => ec) ∈ rules →
                      Δ , Σ' , F ⊢ r ⇐⌊ ⛽ ⌋ C[ c ] ¿¿ := K1 →
                      Δ , Σ' , F ⊢ ec ⌊ ⛽↓ ⌋⇌ ((E ,, (xc , C⁻¹[ c ] r)) , ex) :: [] := K2 →
                      K1 ⊕ K2 := K' →
                      Δ , Σ' , F ⊢ [ E ]case r of⦃· rules ·⦄ ⇐⌊ ⛽ ⌋ ex := K'
      UCaseGuess  : ∀{⛽ ⛽↓ Δ Σ' F F' E r rules ex c xc ec r' A K K' Kₘ₁ Kₘ₂} →
                      ex ≠ ¿¿ →
                      ⛽ ⛽⇓ ⛽↓ →
                      (c , |C xc => ec) ∈ rules →
                      Δ , Σ' ⊢ᴴ F' →
                      F ## F' →
                      F ∪ F' ⊢ r ⌊ ⛽ ⌋⇨ C[ c ] r' := A →
                      Δ , Σ' ⊢Simplify A ⌊ ⛽ ⌋:= K →
                      Δ , Σ' , F ∪ F' ⊢ ec ⌊ ⛽↓ ⌋⇌ ((E ,, (xc , r')) , ex) :: [] := K' →
                      K ⊕ K' := Kₘ₁ →
                      (F' , ∅) ⊕ Kₘ₁ := Kₘ₂ →
                      Δ , Σ' , F ⊢ [ E ]case r of⦃· rules ·⦄ ⇐⌊ ⛽ ⌋ ex := Kₘ₂
      UUnwrapCtor : ∀{⛽ Δ Σ' F c r ex K} →
                      ex ≠ ¿¿ →
                      Δ , Σ' , F ⊢ r ⇐⌊ ⛽ ⌋ C[ c ] ex := K →
                      Δ , Σ' , F ⊢ C⁻¹[ c ] r ⇐⌊ ⛽ ⌋ ex := K

    -- Assertion Simplification
    data _,_⊢Simplify_⌊_⌋:=_ : hctx → denv → assertions → Fuel → constraints → Set where
      SNil : ∀{⛽ Δ Σ'} → Δ , Σ' ⊢Simplify [] ⌊ ⛽ ⌋:= (∅ , ∅)
      SInd : ∀{⛽ Δ Σ' r v A K K' K''} →
               Δ , Σ' ⊢Simplify A ⌊ ⛽ ⌋:= K →
               r final →
               Δ , Σ' , ∅ ⊢ r ⇐⌊ ⛽ ⌋ ⌊ v ⌋ := K' →
               K ⊕ K' := K'' →
               Δ , Σ' ⊢Simplify (r , v) :: A ⌊ ⛽ ⌋:= K''

    -- Live Bidirectional Example Checking
    data _,_,_⊢_⌊_⌋⇌_:=_ : hctx → denv → hole-fillings → exp → Fuel → excons → constraints → Set where
      ChkNil : ∀{⛽ Δ Σ' F e} → Δ , Σ' , F ⊢ e ⌊ ⛽ ⌋⇌ [] := (∅ , ∅)
      ChkInd : ∀{⛽ Δ Σ' F e E ex X r r' A A' K K' K'' Kₘ₁ Kₘ₂} →
                 Δ , Σ' , F ⊢ e ⌊ ⛽ ⌋⇌ X := K →
                 E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ A →
                 F ⊢ r ⌊ ⛽ ⌋⇨ r' := A' →
                 Δ , Σ' , F ⊢ r' ⇐⌊ ⛽ ⌋ ex := K' →
                 Δ , Σ' ⊢Simplify A ++ A' ⌊ ⛽ ⌋:= K'' →
                 K' ⊕ K'' := Kₘ₁ →
                 K ⊕ Kₘ₁ := Kₘ₂ →
                 Δ , Σ' , F ⊢ e ⌊ ⛽ ⌋⇌ ((E , ex) :: X) := Kₘ₂

  -- TODO theorems for all the things, including resumption, synthesis, solve, satisfaction, consistency, Group, and Filter

  -- Type-Directed Guessing
  data _⊢⦇_⊢●:_⦈:=ᴳ_ : denv → tctx → typ → exp → Set where
    GUnit : ∀{Σ' Γ} → Σ' ⊢⦇ Γ ⊢●: ⟨⟩ ⦈:=ᴳ ⟨⟩
    GPair : ∀{Σ' Γ τ1 τ2 e1 e2} →
              Σ' ⊢⦇ Γ ⊢●: τ1 ⦈:=ᴳ e1 →
              Σ' ⊢⦇ Γ ⊢●: τ2 ⦈:=ᴳ e2 →
              Σ' ⊢⦇ Γ ⊢●: ⟨ τ1 × τ2 ⟩ ⦈:=ᴳ ⟨ e1 , e2 ⟩
    GCtor : ∀{Σ' Γ d cctx c τ e} →
              (d , cctx) ∈ π1 Σ' →
              (c , τ) ∈ cctx →
              Σ' ⊢⦇ Γ ⊢●: τ ⦈:=ᴳ e →
              Σ' ⊢⦇ Γ ⊢●: D[ d ] ⦈:=ᴳ (C[ c ] e)
    GFix  : ∀{Σ' Γ τ1 τ2 f x e} →
              Σ' ⊢⦇ Γ ,, (f , τ1 ==> τ2) ,, (x , τ1) ⊢●: τ2 ⦈:=ᴳ e →
              Σ' ⊢⦇ Γ ⊢●: τ1 ==> τ2 ⦈:=ᴳ fix f ⦇·λ x => e ·⦈
    GCase : ∀{Σ' Γ τ e rules d cctx} →
              (d , cctx) ∈ π1 Σ' →
              (∀{c} → dom cctx c → dom rules c) →
              (∀{c} → dom rules c → dom cctx c) →
              Σ' ⊢⦇ Γ ⊢●: D[ d ] ⦈:=ᴳ e →
              (∀{c x-c e-c τ-c} →
                 (c , |C x-c => e-c) ∈ rules →
                 (c , τ-c) ∈ cctx →
                 Σ' ⊢⦇ Γ ,, (x-c , τ-c) ⊢●: τ ⦈:=ᴳ e-c) →
              Σ' ⊢⦇ Γ ⊢●: τ ⦈:=ᴳ case e of⦃· rules ·⦄
    GVar  : ∀{Σ' Γ τ x} →
              (x , τ) ∈ Γ →
              Σ' ⊢⦇ Γ ⊢●: τ ⦈:=ᴳ X[ x ]
    GApp  : ∀{Σ' Γ τ e1 e2 τ'} →
              Σ' ⊢⦇ Γ ⊢●: τ' ==> τ ⦈:=ᴳ e1 →
              Σ' ⊢⦇ Γ ⊢●: τ' ⦈:=ᴳ e2 →
              Σ' ⊢⦇ Γ ⊢●: τ ⦈:=ᴳ (e1 ∘ e2)
    GPrj  : ∀{Σ' Γ τ1 τ2 i e} →
              Σ' ⊢⦇ Γ ⊢●: ⟨ τ1 × τ2 ⟩ ⦈:=ᴳ e →
              Σ' ⊢⦇ Γ ⊢●: prj i τ1 τ2 ⦈:=ᴳ (prj[ i ] e)

  -- TODO theorem that if u # Δ , then u is new in a type-checked exp or result

  -- TODO theorem that any hole in the exp produced by refinement is in the goals

  -- Type-and-Example-Directed Refinement
  data _⊢⦇_⊢●:_⊨_⦈:=ᴿ_⊣_ : denv → tctx → typ → excons → exp → goals → Set where
    RefUnit : ∀{Σ' Γ X Xf} →
                Filter X := Xf →
                (∀{i E ex} → Xf ⟦ i ⟧ == Some (E , ex) → ex == ⟨⟩) →
                Σ' ⊢⦇ Γ ⊢●: ⟨⟩ ⊨ X ⦈:=ᴿ ⟨⟩ ⊣ []
    RefPair : ∀{Σ' Γ τ1 τ2 X u1 u2 G1 G2} {E-ex1-ex2s : List (env ∧ ex ∧ ex)} →
                Filter X := map (λ {(E , ex1 , ex2) → E , ⟨ ex1 , ex2 ⟩}) E-ex1-ex2s →
                G1 == Γ ⊢??[ u1 ]: τ1 ⊨ map (λ {(E , ex1 , ex2) → E , ex1}) E-ex1-ex2s →
                G2 == Γ ⊢??[ u2 ]: τ2 ⊨ map (λ {(E , ex1 , ex2) → E , ex2}) E-ex1-ex2s →
                Σ' ⊢⦇ Γ ⊢●: ⟨ τ1 × τ2 ⟩ ⊨ X ⦈:=ᴿ ⟨ ??[ u1 ] , ??[ u2 ] ⟩ ⊣ (G1 :: (G2 :: []))
    RefCtor : ∀{Σ' Γ X X' d cctx c τ u G} →
                (d , cctx) ∈ π1 Σ' →
                (c , τ) ∈ cctx →
                Filter X := map (λ {(E , ex) → E , C[ c ] ex}) X' →
                G == Γ ⊢??[ u ]: τ ⊨ X' →
                Σ' ⊢⦇ Γ ⊢●: D[ d ] ⊨ X ⦈:=ᴿ C[ c ] ??[ u ] ⊣ (G :: [])
    RefFix  : ∀{Σ' Γ X τ1 τ2 f x u X' G} {E-in-inᶜ-outs : List (env ∧ val ∧ result ∧ ex)} →
                (∀{i E-i v-i r-i ex-i} →
                   E-in-inᶜ-outs ⟦ i ⟧ == Some (E-i , v-i , r-i , ex-i) →
                   ⌈ r-i ⌉:= v-i) →
                Filter X := map (λ {(E , in' , _ , out) → E , in' ↦ out}) E-in-inᶜ-outs →
                X' == map (λ {(E , _ , in' , out) → (E ,, (f , [ E ]fix f ⦇·λ x => ??[ u ] ·⦈) ,, (x , in')) , out}) E-in-inᶜ-outs →
                G == (Γ ,, (f , τ1 ==> τ2) ,, (x , τ1)) ⊢??[ u ]: τ2 ⊨ X' →
                Σ' ⊢⦇ Γ ⊢●: τ1 ==> τ2 ⊨ X ⦈:=ᴿ fix f ⦇·λ x => ??[ u ] ·⦈ ⊣ (G :: [])

  -- Type-and-Example-Directed Branching
  data _⊢⦇_⊢●:_⊨_⦈⌊_⌋:=ᴮ_⊣_ : denv → tctx → typ → excons → Fuel → exp → goals → Set where
    BCase : ∀{⛽ Σ' Γ X Xf τ e rules d cctx x τ+u+X⁺-ctx Gs} →
              Filter X := Xf →
              -- choose one fresh variable name that will be used for all cases
              x # Γ →
              -- τ+u+X⁺-ctx is just cctx extended with hole names and excons
              cctx == ctxmap π1 τ+u+X⁺-ctx →
              -- the rules can be defined from x and the hole names in τ+u+X⁺-ctx
              rules == ctxmap (λ {(τ-c , u-c , X⁺-c) → |C x => ??[ u-c ]}) τ+u+X⁺-ctx →
              -- the following premises appear in the paper
              (d , cctx) ∈ π1 Σ' →
              Σ' ⊢⦇ Γ ⊢●: D[ d ] ⦈:=ᴳ e →
              Gs == map
                 (λ {(τ-c , u-c , X⁺-c) →
                    -- this corresponds to the goal definition in the paper
                    (Γ ,, (x , τ-c)) ⊢??[ u-c ]: τ ⊨
                       -- this corresponds to the definition of each X_i in the paper
                       map (λ {(E , ex , r) → (E ,, (x , r)) , ex}) X⁺-c})
                 (ctx⇒values τ+u+X⁺-ctx) →
              -- the following premise checks that every X⁺-c obeys the rules in the paper premise
              (∀{c τ-c u-c X⁺-c} →
                 (c , τ-c , u-c , X⁺-c) ∈ τ+u+X⁺-ctx →
                 -- for each excon (extended with a result r-j) of X⁺-c, ...
                 (∀{j E-j ex-j r-j} →
                    X⁺-c ⟦ j ⟧ == Some (E-j , ex-j , r-j) →
                      -- the excon is an element of Filter X, and ...
                      Σ[ k ∈ Nat ] (Xf ⟦ k ⟧ == Some (E-j , ex-j)) ∧
                      -- the scrutinee e will evaluate to constructor c applied to the specified argument r-j
                      E-j ⊢ e ⌊ ⛽ ⌋⇒ C[ c ] r-j ⊣ [])) →
              -- the last premise in the paper - every excon in Filter X is an element of some X⁺-c for some c
              (∀{k E-k ex-k} →
                 Xf ⟦ k ⟧ == Some (E-k , ex-k) →
                 Σ[ c ∈ Nat ] Σ[ τ-c ∈ typ ] Σ[ u-c ∈ Nat ] Σ[ X⁺-c ∈ List (env ∧ ex ∧ result)] Σ[ j ∈ Nat ] Σ[ r-j ∈ result ] (
                    (c , τ-c , u-c , X⁺-c) ∈ τ+u+X⁺-ctx ∧
                    X⁺-c ⟦ j ⟧ == Some (E-k , ex-k , r-j))) →
              Σ' ⊢⦇ Γ ⊢●: τ ⊨ X ⦈⌊ ⛽ ⌋:=ᴮ case e of⦃· rules ·⦄ ⊣ Gs

  -- Hole Filling
  data _,_,_⊢⦇_⊢??[_]:_⊨_⦈⌊_⌋:=_,_ : hctx → denv → hole-fillings → tctx → Nat → typ → excons → Fuel → constraints → hctx → Set where
    HFRefBranch : ∀{⛽ Δ Σ' F Γ u τ X e Gs K Δ'} →
                    -- this premise ensures that all holes are fresh
                    (∀{i j g-i g-j} →
                       Gs ⟦ i ⟧ == Some g-i →
                       Gs ⟦ j ⟧ == Some g-j →
                         goal.g-id g-i # Δ ∧
                         goal.g-id g-i ≠ u ∧
                         (i ≠ j → goal.g-id g-i ≠ goal.g-id g-j)) →
                    (Σ' ⊢⦇ Γ ⊢●: τ ⊨ X ⦈:=ᴿ e ⊣ Gs ∨
                     Σ' ⊢⦇ Γ ⊢●: τ ⊨ X ⦈⌊ ⛽ ⌋:=ᴮ e ⊣ Gs) →
                    K == (■ (u , e) , list⇒ctx (map (λ {(_ ⊢??[ u' ]: _ ⊨ X') → u' , X'}) Gs)) →
                    Δ' == list⇒ctx (map (λ {(Γ' ⊢??[ u' ]: τ' ⊨ _) → u' , Γ' , τ'}) Gs) →
                    Δ , Σ' , F ⊢⦇ Γ ⊢??[ u ]: τ ⊨ X ⦈⌊ ⛽ ⌋:= K , Δ'
    HFGuessChk  : ∀{⛽ Δ Σ' F Γ u τ X e K K'} →
                    Σ' ⊢⦇ Γ ⊢●: τ ⦈:=ᴳ e →
                    Δ , Σ' , (F ,, (u , e)) ⊢ e ⌊ ⛽ ⌋⇌ X := K →
                    (■ (u , e) , ∅) ⊕ K := K' →
                    Δ , Σ' , F ⊢⦇ Γ ⊢??[ u ]: τ ⊨ X ⦈⌊ ⛽ ⌋:= K' , ∅
    HFDefer     : ∀{⛽ Δ Σ' F Γ u τ X} →
                    X ≠ [] →
                    Filter X := [] →
                    Δ , Σ' , F ⊢⦇ Γ ⊢??[ u ]: τ ⊨ X ⦈⌊ ⛽ ⌋:= (■ (u , ??[ u ]) , ∅) , ∅

  {- TODO - later, we need to fix this stuff up too
  data _,_IterSolve_,_⌊_⌋:=_,_ : hctx → denv → hole-fillings → excons ctx → Fuel → hole-fillings → hctx → Set where
    ISFin : ∀{⛽ Δ Σ' F-0 U F' Δ' u+F+Δs} →
              (∀{u} → dom U u → dom Δ u) →
              ∥ u+F+Δs ∥ == 1+ ∥ U ∥ →
              Σ[ u-0 ∈ Nat ] (u+F+Δs ⟦ 0 ⟧ == Some (u-0 , F-0 , Δ)) →
              (∀{u W} →
                 (u , W) ∈ U →
                 Σ[ i ∈ Nat ] Σ[ F-i ∈ hole-fillings ] Σ[ Δ-i ∈ hctx ] (
                    1+ i < ∥ u+F+Δs ∥ ∧ u+F+Δs ⟦ i ⟧ == Some (u , F-i , Δ-i))) →
              (∀{i u-i u-i+1 W-i F-i F-i+1 Δ-i Δ-i+1 Γ-i τ-i} →
                 1+ i < ∥ u+F+Δs ∥ →
                 u+F+Δs ⟦ i ⟧    == Some (u-i , F-i , Δ-i) →
                 u+F+Δs ⟦ 1+ i ⟧ == Some (u-i+1 , F-i+1 , Δ-i+1) →
                 (u-i , W-i) ∈ U →
                 (u-i , Γ-i , τ-i) ∈ Δ →
                 Σ[ F'-i ∈ hole-fillings ] Σ[ Δ'-i ∈ hctx ] (
                    (Δ-i , Σ' , F-i ⊢⦇ Γ-i ⊢??[ u-i ]: τ-i ⊨ W-i ⦈⌊ ⛽ ⌋:= (F'-i , ∅) , Δ'-i) ∧
                    F-i+1 == F-i ∪ F'-i ∧
                    Δ-i+1 == Δ-i ∪ Δ'-i)) →
              Σ[ u-n ∈ Nat ] (u+F+Δs ⟦ ∥ U ∥ ⟧ == Some (u-n , F' , Δ')) →
              Δ , Σ' IterSolve F-0 , U ⌊ ⛽ ⌋:= F' , Δ'
    ISInd : ∀{⛽ Δ Σ' F-0 U F' Δ' u+F+U+Δs U' Δ-n F-n} →
              (∀{u} → dom U u → dom Δ u) →
              ∥ u+F+U+Δs ∥ == 1+ ∥ U ∥ →
              Σ[ u-0 ∈ Nat ] (u+F+U+Δs ⟦ 0 ⟧ == Some (u-0 , F-0 , ∅ , Δ)) →
              (∀{u W} →
                 (u , W) ∈ U →
                 Σ[ i ∈ Nat ] Σ[ F-i ∈ hole-fillings ] Σ[ U-i ∈ excons ctx ] Σ[ Δ-i ∈ hctx ] (
                    1+ i < ∥ u+F+U+Δs ∥ ∧ u+F+U+Δs ⟦ i ⟧ == Some (u , F-i , U-i , Δ-i))) →
              (∀{i u-i u-i+1 W-i F-i F-i+1 U-i U-i+1 Δ-i Δ-i+1 Γ-i τ-i} →
                 1+ i < ∥ u+F+U+Δs ∥ →
                 u+F+U+Δs ⟦ i ⟧    == Some (u-i , F-i , U-i , Δ-i) →
                 u+F+U+Δs ⟦ 1+ i ⟧ == Some (u-i+1 , F-i+1 , U-i+1 , Δ-i+1) →
                 (u-i , W-i) ∈ U →
                 (u-i , Γ-i , τ-i) ∈ Δ →
                 Σ[ F'-i ∈ hole-fillings ] Σ[ Δ'-i ∈ hctx ] (
                    (Δ-i , Σ' , F-i ⊢⦇ Γ-i ⊢??[ u-i ]: τ-i ⊨ W-i ⦈⌊ ⛽ ⌋:= (F'-i , U-i+1) , Δ'-i) ∧
                    F-i+1 == F-i ∪ F'-i ∧
                    Δ-i+1 == Δ-i ∪ Δ'-i)) →
              U' == foldl _∪_ ∅ (map (π1 ⊙ (π2 ⊙ π2)) u+F+U+Δs) →
              U' ≠ ∅ →
              Σ[ u-n ∈ Nat ] Σ[ U-n ∈ excons ctx ] (u+F+U+Δs ⟦ ∥ U ∥ ⟧ == Some (u-n , F-n , U-n , Δ-n)) →
              Δ-n , Σ' IterSolve F-n , U' ⌊ ⛽ ⌋:= F' , Δ' →
              Δ , Σ' IterSolve F-0 , U ⌊ ⛽ ⌋:= F' , Δ'

  data _,_Solve_⌊_⌋:=_ : hctx → denv → constraints → Fuel → hole-fillings → Set where
    Solve : ∀{⛽ Δ Σ' F0 U F Δ'} →
              Δ , Σ' IterSolve F0 , U ⌊ ⛽ ⌋:= F , Δ' →
              Δ , Σ' Solve (F0 , U) ⌊ ⛽ ⌋:= F
  -}

{- TODO

  -- those external expressions without holes
  data _ecomplete : hexp → Set where
    ECConst : c ecomplete
    ECAsc : ∀{τ e} → τ tcomplete → e ecomplete → (e ·: τ) ecomplete
    ECVar : ∀{x} → (X x) ecomplete
    ECLam1 : ∀{x e} → e ecomplete → (·λ x e) ecomplete
    ECLam2 : ∀{x e τ} → e ecomplete → τ tcomplete → (·λ x [ τ ] e) ecomplete
    ECAp : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → (e1 ∘ e2) ecomplete
    ECFst : ∀{e} → e ecomplete → (fst e) ecomplete
    ECSnd : ∀{e} → e ecomplete → (snd e) ecomplete
    ECPair : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → ⟨ e1 , e2 ⟩ ecomplete

  -- those internal expressions without holes
  data _dcomplete : ihexp → Set where
    DCVar : ∀{x} → (X x) dcomplete
    DCConst : c dcomplete
    DCLam : ∀{x τ d} → d dcomplete → τ tcomplete → (·λ x [ τ ] d) dcomplete
    DCAp : ∀{d1 d2} → d1 dcomplete → d2 dcomplete → (d1 ∘ d2) dcomplete
    DCCast : ∀{d τ1 τ2} → d dcomplete → τ1 tcomplete → τ2 tcomplete → (d ⟨ τ1 ⇒ τ2 ⟩) dcomplete
    DCFst : ∀{d} → d dcomplete → (fst d) dcomplete
    DCSnd : ∀{d} → d dcomplete → (snd d) dcomplete
    DCPair : ∀{d1 d2} → d1 dcomplete → d2 dcomplete → ⟨ d1 , d2 ⟩ dcomplete

  mutual
    -- substitution typing
    data _,_⊢_:s:_ : hctx → tctx → env → tctx → Set where
      STAId : ∀{Γ Γ' Δ} →
                  ((x : Nat) (τ : htyp) → (x , τ) ∈ Γ' → (x , τ) ∈ Γ) →
                  Δ , Γ ⊢ Id Γ' :s: Γ'
      STASubst : ∀{Γ Δ σ y Γ' d τ } →
               Δ , Γ ,, (y , τ) ⊢ σ :s: Γ' →
               Δ , Γ ⊢ d :: τ →
               Δ , Γ ⊢ Subst d y σ :s: Γ'

    -- type assignment
    data _,_⊢_::_ : (Δ : hctx) (Γ : tctx) (d : ihexp) (τ : htyp) → Set where
      TAConst : ∀{Δ Γ} → Δ , Γ ⊢ c :: b
      TAVar : ∀{Δ Γ x τ} → (x , τ) ∈ Γ → Δ , Γ ⊢ X x :: τ
      TALam : ∀{ Δ Γ x τ1 d τ2} →
              x # Γ →
              Δ , (Γ ,, (x , τ1)) ⊢ d :: τ2 →
              Δ , Γ ⊢ ·λ x [ τ1 ] d :: (τ1 ==> τ2)
      TAAp : ∀{ Δ Γ d1 d2 τ1 τ} →
             Δ , Γ ⊢ d1 :: τ1 ==> τ →
             Δ , Γ ⊢ d2 :: τ1 →
             Δ , Γ ⊢ d1 ∘ d2 :: τ
      TAEHole : ∀{ Δ Γ σ u Γ' τ} →
                (u , (Γ' , τ)) ∈ Δ →
                Δ , Γ ⊢ σ :s: Γ' →
                Δ , Γ ⊢ ⦇⦈⟨ u , σ ⟩ :: τ
      TANEHole : ∀ { Δ Γ d τ' Γ' u σ τ } →
                 (u , (Γ' , τ)) ∈ Δ →
                 Δ , Γ ⊢ d :: τ' →
                 Δ , Γ ⊢ σ :s: Γ' →
                 Δ , Γ ⊢ ⦇⌜ d ⌟⦈⟨ u , σ ⟩ :: τ
      TACast : ∀{ Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 →
             τ1 ~ τ2 →
             Δ , Γ ⊢ d ⟨ τ1 ⇒ τ2 ⟩ :: τ2
      TAFailedCast : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 →
             τ1 ground →
             τ2 ground →
             τ1 ≠ τ2 →
             Δ , Γ ⊢ d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩ :: τ2
      TAFst : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 ⊗ τ2 →
             Δ , Γ ⊢ fst d :: τ1
      TASnd : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 ⊗ τ2 →
             Δ , Γ ⊢ snd d :: τ2
      TAPair : ∀{Δ Γ d1 d2 τ1 τ2} →
             Δ , Γ ⊢ d1 :: τ1 →
             Δ , Γ ⊢ d2 :: τ2 →
             Δ , Γ ⊢ ⟨ d1 , d2 ⟩ :: τ1 ⊗ τ2

  -- substitution
  [_/_]_ : ihexp → Nat → ihexp → ihexp
  [ d / y ] c = c
  [ d / y ] X x
    with natEQ x y
  [ d / y ] X .y | Inl refl = d
  [ d / y ] X x  | Inr neq = X x
  [ d / y ] (·λ x [ x₁ ] d')
    with natEQ x y
  [ d / y ] (·λ .y [ τ ] d') | Inl refl = ·λ y [ τ ] d'
  [ d / y ] (·λ x [ τ ] d')  | Inr x₁ = ·λ x [ τ ] ( [ d / y ] d')
  [ d / y ] ⦇⦈⟨ u , σ ⟩ = ⦇⦈⟨ u , Subst d y σ ⟩
  [ d / y ] ⦇⌜ d' ⌟⦈⟨ u , σ  ⟩ =  ⦇⌜ [ d / y ] d' ⌟⦈⟨ u , Subst d y σ ⟩
  [ d / y ] (d1 ∘ d2) = ([ d / y ] d1) ∘ ([ d / y ] d2)
  [ d / y ] (d' ⟨ τ1 ⇒ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒ τ2 ⟩
  [ d / y ] (d' ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩
  [ d / y ] ⟨ d1 , d2 ⟩ = ⟨ [ d / y ] d1 , [ d / y ] d2 ⟩
  [ d / y ] (fst d') = fst ([ d / y ] d')
  [ d / y ] (snd d') = snd ([ d / y ] d')

  -- applying an environment to an expression
  apply-env : env → ihexp → ihexp
  apply-env (Id Γ) d = d
  apply-env (Subst d y σ) d' = [ d / y ] ( apply-env σ d')

  -- freshness
  mutual
    -- ... with respect to a hole context
    data envfresh : Nat → env → Set where
      EFId : ∀{x Γ} → x # Γ → envfresh x (Id Γ)
      EFSubst : ∀{x d σ y} → fresh x d
                           → envfresh x σ
                           → x ≠ y
                           → envfresh x (Subst d y σ)

    -- ... for inernal expressions
    data fresh : Nat → ihexp → Set where
      FConst : ∀{x} → fresh x c
      FVar   : ∀{x y} → x ≠ y → fresh x (X y)
      FLam   : ∀{x y τ d} → x ≠ y → fresh x d → fresh x (·λ y [ τ ] d)
      FHole  : ∀{x u σ} → envfresh x σ → fresh x (⦇⦈⟨ u , σ ⟩)
      FNEHole : ∀{x d u σ} → envfresh x σ → fresh x d → fresh x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      FAp     : ∀{x d1 d2} → fresh x d1 → fresh x d2 → fresh x (d1 ∘ d2)
      FCast   : ∀{x d τ1 τ2} → fresh x d → fresh x (d ⟨ τ1 ⇒ τ2 ⟩)
      FFailedCast : ∀{x d τ1 τ2} → fresh x d → fresh x (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
      FFst  : ∀{x d} → fresh x d → fresh x (fst d)
      FSnd  : ∀{x d} → fresh x d → fresh x (snd d)
      FPair : ∀{x d1 d2} → fresh x d1 → fresh x d2 → fresh x ⟨ d1 , d2 ⟩

  -- ... for external expressions
  data freshh : Nat → hexp → Set where
    FRHConst : ∀{x} → freshh x c
    FRHAsc   : ∀{x e τ} → freshh x e → freshh x (e ·: τ)
    FRHVar   : ∀{x y} → x ≠ y → freshh x (X y)
    FRHLam1  : ∀{x y e} → x ≠ y → freshh x e → freshh x (·λ y e)
    FRHLam2  : ∀{x τ e y} → x ≠ y → freshh x e → freshh x (·λ y [ τ ] e)
    FRHEHole : ∀{x u} → freshh x (⦇⦈[ u ])
    FRHNEHole : ∀{x u e} → freshh x e → freshh x (⦇⌜ e ⌟⦈[ u ])
    FRHAp : ∀{x e1 e2} → freshh x e1 → freshh x e2 → freshh x (e1 ∘ e2)
    FRHFst  : ∀{x e} → freshh x e → freshh x (fst e)
    FRHSnd  : ∀{x e} → freshh x e → freshh x (snd e)
    FRHPair : ∀{x e1 e2} → freshh x e1 → freshh x e2 → freshh x ⟨ e1 , e2 ⟩

  -- with respect to all bindings in a context
  freshΓ : {A : Set} → (Γ : A ctx) → (e : hexp) → Set
  freshΓ {A} Γ e = (x : Nat) → dom Γ x → freshh x e

  -- x is not used in a binding site in d
  mutual
    data unbound-in-σ : Nat → env → Set where
      UBσId : ∀{x Γ} → unbound-in-σ x (Id Γ)
      UBσSubst : ∀{x d y σ} → unbound-in x d
                            → unbound-in-σ x σ
                            → x ≠ y
                            → unbound-in-σ x (Subst d y σ)

    data unbound-in : (x : Nat) (d : ihexp) → Set where
      UBConst : ∀{x} → unbound-in x c
      UBVar : ∀{x y} → unbound-in x (X y)
      UBLam2 : ∀{x d y τ} → x ≠ y
                           → unbound-in x d
                           → unbound-in x (·λ_[_]_ y τ d)
      UBHole : ∀{x u σ} → unbound-in-σ x σ
                         → unbound-in x (⦇⦈⟨ u , σ ⟩)
      UBNEHole : ∀{x u σ d }
                  → unbound-in-σ x σ
                  → unbound-in x d
                  → unbound-in x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      UBAp : ∀{ x d1 d2 } →
            unbound-in x d1 →
            unbound-in x d2 →
            unbound-in x (d1 ∘ d2)
      UBCast : ∀{x d τ1 τ2} → unbound-in x d → unbound-in x (d ⟨ τ1 ⇒ τ2 ⟩)
      UBFailedCast : ∀{x d τ1 τ2} → unbound-in x d → unbound-in x (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
      UBFst  : ∀{x d} → unbound-in x d → unbound-in x (fst d)
      UBSnd  : ∀{x d} → unbound-in x d → unbound-in x (snd d)
      UBPair : ∀{x d1 d2} → unbound-in x d1 → unbound-in x d2 → unbound-in x ⟨ d1 , d2 ⟩

  mutual
    data binders-disjoint-σ : env → ihexp → Set where
      BDσId : ∀{Γ d} → binders-disjoint-σ (Id Γ) d
      BDσSubst : ∀{d1 d2 y σ} → binders-disjoint d1 d2
                              → binders-disjoint-σ σ d2
                              → binders-disjoint-σ (Subst d1 y σ) d2

    -- two terms that do not share any binders
    data binders-disjoint : (d1 : ihexp) → (d2 : ihexp) → Set where
      BDConst : ∀{d} → binders-disjoint c d
      BDVar : ∀{x d} → binders-disjoint (X x) d
      BDLam : ∀{x τ d1 d2} → binders-disjoint d1 d2
                            → unbound-in x d2
                            → binders-disjoint (·λ_[_]_ x τ d1) d2
      BDHole : ∀{u σ d2} → binders-disjoint-σ σ d2
                         → binders-disjoint (⦇⦈⟨ u , σ ⟩) d2
      BDNEHole : ∀{u σ d1 d2} → binders-disjoint-σ σ d2
                              → binders-disjoint d1 d2
                              → binders-disjoint (⦇⌜ d1 ⌟⦈⟨ u , σ ⟩) d2
      BDAp :  ∀{d1 d2 d3} → binders-disjoint d1 d3
                          → binders-disjoint d2 d3
                          → binders-disjoint (d1 ∘ d2) d3
      BDCast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint (d1 ⟨ τ1 ⇒ τ2 ⟩) d2
      BDFailedCast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint (d1 ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩) d2
      BDFst  : ∀{d1 d2} → binders-disjoint d1 d2 → binders-disjoint (fst d1) d2
      BDSnd  : ∀{d1 d2} → binders-disjoint d1 d2 → binders-disjoint (snd d1) d2
      BDPair : ∀{d1 d2 d3} →
               binders-disjoint d1 d3 →
               binders-disjoint d2 d3 →
               binders-disjoint ⟨ d1 , d2 ⟩ d3

  mutual
  -- each term has to be binders unique, and they have to be pairwise
  -- disjoint with the collection of bound vars
    data binders-unique-σ : env → Set where
      BUσId : ∀{Γ} → binders-unique-σ (Id Γ)
      BUσSubst : ∀{d y σ} → binders-unique d
                          → binders-unique-σ σ
                          → binders-disjoint-σ σ d
                          → binders-unique-σ (Subst d y σ)

    -- all the variable names in the term are unique
    data binders-unique : ihexp → Set where
      BUHole : binders-unique c
      BUVar : ∀{x} → binders-unique (X x)
      BULam : {x : Nat} {τ : htyp} {d : ihexp} → binders-unique d
                                                → unbound-in x d
                                                → binders-unique (·λ_[_]_ x τ d)
      BUEHole : ∀{u σ} → binders-unique-σ σ
                        → binders-unique (⦇⦈⟨ u , σ ⟩)
      BUNEHole : ∀{u σ d} → binders-unique d
                           → binders-unique-σ σ
                           → binders-unique (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      BUAp : ∀{d1 d2} → binders-unique d1
                       → binders-unique d2
                       → binders-disjoint d1 d2
                       → binders-unique (d1 ∘ d2)
      BUCast : ∀{d τ1 τ2} → binders-unique d
                           → binders-unique (d ⟨ τ1 ⇒ τ2 ⟩)
      BUFailedCast : ∀{d τ1 τ2} → binders-unique d
                                 → binders-unique (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
      BUFst  : ∀{d} →
               binders-unique d →
               binders-unique (fst d)
      BUSnd  : ∀{d} →
               binders-unique d →
               binders-unique (snd d)
      BUPair : ∀{d1 d2} →
               binders-unique d1 →
               binders-unique d2 →
               binders-disjoint d1 d2 →
               binders-unique ⟨ d1 , d2 ⟩

-}

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae

module ClassicalLogic.ClassicalFive where

em = {A : Set} → (A || (A → False))
dne = {A : Set} → ((A → False) → False) → A
peirce = {A B : Set} → ((A → B) → A) → A
iad = {A B : Set} → (A → B) → ((A → False) || B)
dem = {A B : Set} → (((A → False) && (B → False)) → False) → A || B

emToDne : em → dne
emToDne em {A} pr with em {A}
emToDne em {A} pr | inl x = x
emToDne em {A} pr | inr x = exFalso (pr x)

dneToPeirce : dne → peirce
dneToPeirce dne {A} {B} aba = dne (λ z → z (aba (λ a → dne (λ _ → z a))))

peirceToIad : peirce → iad
peirceToIad peirce {A} {B} aToB = peirce (λ z → inl (λ x → z (inr (aToB x))))

iadToDem : iad → dem
iadToDem iad {A} {B} x with iad {A} {A} (λ i → i)
iadToDem iad {A} {B} x | inl notA with iad {B} {B} (λ i → i)
iadToDem iad {A} {B} x | inl notA | inl notB = exFalso (x (notA ,, notB))
iadToDem iad {A} {B} x | inl notA | inr b = inr b
iadToDem iad {A} {B} x | inr a = inl a

demToEm : dem → em
demToEm dem {A} = dem (λ z → _&&_.snd z (_&&_.fst z))

ext: agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Concrete.Records as LCR
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.KVMap
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude
open import Yasm.Base

open        EpochConfig

-- This module contains placeholders for the future analog of the
-- corresponding VotesOnce property.  Defining the implementation
-- obligation and proving that it is an invariant of an implementation
-- is a substantial undertaking.  We are working first on proving the
-- simpler VotesOnce property to settle down the structural aspects
-- before tackling the harder semantic issues.
module LibraBFT.Concrete.Properties.PreferredRound (iiah : SystemInitAndHandlers ℓ-RoundManager ConcSysParms) (𝓔 : EpochConfig) where
 open        LibraBFT.ImplShared.Consensus.Types.EpochDep.WithEC
 import      LibraBFT.Abstract.Records         UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs
 import      LibraBFT.Abstract.Records.Extends UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Ext
 open import LibraBFT.Abstract.RecordChain     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔)
 open import LibraBFT.Abstract.System          UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔)
 open import LibraBFT.Concrete.Intermediate                      𝓔 (ConcreteVoteEvidence 𝓔)
 open import LibraBFT.Concrete.Obligations.PreferredRound        𝓔 (ConcreteVoteEvidence 𝓔)
 open        SystemTypeParameters ConcSysParms
 open        SystemInitAndHandlers iiah
 open        ParamsWithInitAndHandlers iiah
 open import LibraBFT.ImplShared.Util.HashCollisions iiah
 open import LibraBFT.Concrete.Properties.Common iiah 𝓔
 open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms iiah PeerCanSignForPK PeerCanSignForPK-stable

 open PerEpoch    𝓔
 open WithAbsVote 𝓔
 open LCR.WithEC  𝓔
 open PerState
 open PerReachableState
 open IntermediateSystemState
 open All-InSys-props

 Block-RC-AllInSys : Abs.Vote → SystemState → Set
 Block-RC-AllInSys vabs st = ∃[ b ] ( Abs.bId b ≡ abs-vBlockUID vabs
                                    × Σ (RecordChain (Abs.B b)) (All-InSys (InSys (intSystemState st))))

 ImplObligation-RC : Set (ℓ+1 ℓ-RoundManager)
 ImplObligation-RC =
   ∀{pid s' outs pk}{pre : SystemState}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → ∀{v m} → Meta-Honest-PK pk
   -- For signed every vote v of every outputted message
   → v ⊂Msg m → send m ∈ outs
   → (sig : WithVerSig pk v)
   → 0 < v ^∙ vRound
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre))
   → let post = StepPeer-post {pre = pre} (step-honest sps)
     in (pcs4 : PeerCanSignForPK post v pid pk)
        → ∃[ mbr ] ( getPubKey 𝓔 mbr ≡ pk
                   × Block-RC-AllInSys (α-ValidVote 𝓔 v mbr) post)

 -- For PreferredRound, we have two implementation obligations, one for when v is sent by the
 -- step and v' has been sent before, and one for when both are sent by the step.
 ImplObligation₁ : Set (ℓ+1 ℓ-RoundManager)
 ImplObligation₁ =
   ∀{pid pid' s' outs pk}{pre : SystemState}
   → (r : ReachableSystemState pre)
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → let post = StepPeer-post {pre = pre} (step-honest sps) in
     ∀{mbr v vabs m v' v'abs m'}
   → Meta-Honest-PK pk
   -- For signed every vote v of every outputted message
   → v'  ⊂Msg m'  → send m' ∈ outs
   → (sig' : WithVerSig pk v') → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig'))
   -- If v is really new and valid
   → ¬ (MsgWithSig∈ pk (ver-signature sig') (msgPool pre))
   → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v' pid pk
   -- And if there exists another v' that has been sent before
   → v ⊂Msg m → (pid' , m) ∈ (msgPool pre)
   → (sig : WithVerSig pk v) → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig))
   -- If v and v' share the same epoch
   → v ^∙  vEpoch ≡ v' ^∙ vEpoch
   -- and v is for a smaller round
   → v ^∙ vRound < v' ^∙ vRound
   -- and vabs* are the abstract Votes for v and v'
   → α-ValidVote 𝓔 v  mbr ≡ vabs
   → α-ValidVote 𝓔 v' mbr ≡ v'abs
   → (c2 : Cand-3-chain-vote (intSystemState post) vabs)
   -- then the round of the block that v' votes for is at least the round of
   -- the grandparent of the block that v votes for (i.e., the preferred round rule)
   → Σ (VoteParentData (intSystemState post) v'abs)
           (λ vp → Cand-3-chain-head-round (intSystemState post) c2 ≤ Abs.round (vpParent vp))
     ⊎ (VoteForRound∈ pk (v' ^∙ vRound) (v' ^∙ vEpoch) (v' ^∙ vProposedId) (msgPool pre))

 -- Similarly in case the same step sends both v and v'
 ImplObligation₂ : Set (ℓ+1 ℓ-RoundManager)
 ImplObligation₂ =
   ∀{pid s' outs pk}{pre : SystemState}
   → (r  : ReachableSystemState pre)
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → let post = StepPeer-post {pre = pre} (step-honest sps) in
     ∀{mbr v vabs m v' v'abs m'}
   → Meta-Honest-PK pk
   -- For every vote v represented in a message output by the call
   → v  ⊂Msg m  → send m ∈ outs
   → (sig : WithVerSig pk v) → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig))
   -- If v is really new and valid
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre))
   → PeerCanSignForPK post v pid pk
   -- And if there exists another v' that is also new and valid
   → v' ⊂Msg m'  → send m' ∈ outs
   → (sig' : WithVerSig pk v') → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig'))
   → ¬ (MsgWithSig∈ pk (ver-signature sig') (msgPool pre))
   → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v' pid pk
   -- If v and v' share the same epoch and round
   → v ^∙ vEpoch ≡ v' ^∙ vEpoch
   → v ^∙ vRound < v' ^∙ vRound
   → α-ValidVote 𝓔 v  mbr ≡ vabs
   → α-ValidVote 𝓔 v' mbr ≡ v'abs
   → (c2 : Cand-3-chain-vote (intSystemState post) vabs)
   → Σ (VoteParentData (intSystemState post) v'abs)
           (λ vp → Cand-3-chain-head-round (intSystemState post) c2 ≤ Abs.round (vpParent vp))

 module _ where
   open InSys iiah

   stepPreservesVoteParentData : ∀ {st0 st1 v}
     → Step st0 st1
     → (vpd : VoteParentData (intSystemState st0) v)
     → Σ (VoteParentData (intSystemState st1) v)
         λ vpd' → vpParent vpd' ≡ vpParent vpd
   stepPreservesVoteParentData {st0} {st1} theStep vpd
      with vpd
   ...| (record { vpV4B        = vpV4B
                ; vpBlock∈sys  = vpBlock∈sys
                ; vpParent     = vpParent
                ; vpParent∈sys = vpParent∈sys
                ; vpExt        = vpExt
                ; vpMaybeBlock = vpMaybeBlock
                }) = (record
                     { vpV4B        = vpV4B
                     ; vpBlock∈sys  = stable theStep vpBlock∈sys
                     ; vpParent     = vpParent
                     ; vpParent∈sys = stable theStep vpParent∈sys
                     ; vpExt        = vpExt
                     ; vpMaybeBlock = transp-vpmb vpMaybeBlock
                     }) , refl
     where transp-vpmb : ∀ {r}
                         → VoteParentData-BlockExt (intSystemState st0) r
                         → VoteParentData-BlockExt (intSystemState st1) r
           transp-vpmb vpParent≡I = vpParent≡I
           transp-vpmb (vpParent≡Q x x₁) = vpParent≡Q x (stable theStep x₁)

 module Proof
   (sps-corr   : StepPeerState-AllValidParts)   -- Bring in newMsg⊎msgSentB4
   (Impl-bsvr  : ImplObl-bootstrapVotesRound≡0)
   (Impl-nvr≢0 : ImplObl-NewVoteRound≢0)
   (Impl-∈BI?  : (sig : Signature) → Dec (∈BootstrapInfo bootstrapInfo sig))
   (Impl-RC    : ImplObligation-RC)
   (Impl-IRO   : IncreasingRoundObligation)
   (Impl-PR1   : ImplObligation₁)
   (Impl-PR2   : ImplObligation₂)
    where
  module _ {st : SystemState}(r : ReachableSystemState st) (𝓔-∈sys : EpochConfig∈Sys st 𝓔) where
   open        Structural sps-corr
   open        ConcreteCommonProperties st r sps-corr Impl-bsvr Impl-nvr≢0

   α-ValidVote-trans : ∀ {pk mbr vabs pool} (v : Vote)
                     → α-ValidVote 𝓔 v mbr ≡ vabs
                     → (vfr : VoteForRound∈ pk (v ^∙ vRound) (v ^∙ vEpoch)
                                            (v ^∙ vProposedId) pool)
                     → α-ValidVote 𝓔 (msgVote vfr) mbr ≡ vabs
   α-ValidVote-trans v₁ refl vfr
     with msgRound≡ vfr | msgEpoch≡ vfr | msgBId≡ vfr
   ...| refl | refl | refl = refl

   0<rnd⇒¬BootStrap : ∀ {pk rnd bid pool}
                      → (v4r : VoteForRound∈ pk rnd (epoch 𝓔) bid pool)
                      → 0 < rnd
                      → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature $ msgSigned v4r))
   0<rnd⇒¬BootStrap v4r 0<r rewrite sym (msgRound≡ v4r) = ⊥-elim ∘ (<⇒≢ 0<r) ∘ sym ∘ Impl-bsvr (msgSigned v4r)

   -- To prove this, we observe that cheaters can't introduce a VoteForRound∈ for an honest PK.  We
   -- will also require an additional implementation obligation.  It may simply be that Votes sent
   -- satisy IsValidVote, but the question is where do we maintain evidence that such a RecordChain
   -- exists for any Block we may vote for?
   voteForRound-RC : ∀ {pk vabs}{st : SystemState}
                     → Meta-Honest-PK pk
                     → ReachableSystemState st
                     → (v4r : VoteForRound∈ pk (abs-vRound vabs) (epoch 𝓔) (abs-vBlockUID vabs) (msgPool st))
                     → 0 < abs-vRound vabs
                     → Block-RC-AllInSys vabs st

   voteForRound-RC-mws : ∀ {pk vabs pre pid st' outs}
                       → Meta-Honest-PK pk
                       → ReachableSystemState pre
                       → (sp : StepPeer pre pid st' outs)
                       → (v4r : VoteForRound∈ pk (abs-vRound vabs) (epoch 𝓔) (abs-vBlockUID vabs) (msgPool $ StepPeer-post sp))
                       → MsgWithSig∈ pk (ver-signature $ msgSigned v4r) (msgPool pre)
                       → 0 < abs-vRound vabs
                       → Block-RC-AllInSys vabs (StepPeer-post sp)
   voteForRound-RC-mws {pk} {vabs} {pre} hpk preReach sps v4r mwsb4 0<r
      with sameSig⇒sameVoteData (msgSigned mwsb4) (msgSigned v4r) (msgSameSig mwsb4)
   ...| inj₁ hb = ⊥-elim $ meta-no-collision preReach hb -- TODO-2: refine sameSig⇒samevotedata to
                                                         -- enable tying collision to specific state
                                                         -- so we can use meta-no-collision-in-sys
   ...| inj₂ svd
      with msgSentB4⇒VoteRound∈ (msgSigned v4r) mwsb4'
         where
           mwsb4' : _
           mwsb4' rewrite
                    trans (cong (_^∙ vdProposed ∙ biEpoch) $ sym svd) (msgEpoch≡ v4r) |
                    msgBId≡ v4r |
                    msgSameSig mwsb4 = mwsb4
   ...| v4r' , refl
      with voteForRound-RC {pk} {vabs} hpk preReach v4r'' 0<r
         where
           v4r'' : VoteForRound∈ pk (abs-vRound vabs) (epoch 𝓔) (abs-vBlockUID vabs) (msgPool pre)
           v4r'' rewrite sym (msgEpoch≡ v4r) | sym (msgRound≡ v4r) | sym (msgBId≡ v4r) = v4r'
   ...| b , refl , rc , ais = b , refl , rc , InSys.ais-stable iiah (step-peer sps) rc ais

   voteForRound-RC {pk} {vabs} {st} hpk (step-s preReach (step-peer (step-honest sps))) v4r 0<r
      with newMsg⊎msgSentB4 {sndr = msgSender v4r} preReach sps hpk (msgSigned v4r)
                            (0<rnd⇒¬BootStrap v4r 0<r)
                            (msg⊆ v4r)
                            (msg∈pool v4r)
   ...| inj₂ mwsb4 = voteForRound-RC-mws {vabs = vabs} hpk preReach (step-honest sps) v4r mwsb4 0<r
   ...| inj₁ (send∈outs , pcs4 , ¬sentb4) rewrite sym (msgRound≡ v4r)
      with Impl-RC preReach sps hpk (msg⊆ v4r) send∈outs (msgSigned v4r) 0<r ¬sentb4 pcs4
   ...| mbr , refl , b , bid≡ , rc∈sys  = b , (trans bid≡ $ msgBId≡ v4r) , rc∈sys
   voteForRound-RC {pk} {vabs} {st} hpk (step-s {pre = pre} preReach (step-peer (step-cheat {pid} x))) v4r 0<r
      with VoteRound∈⇒msgSent v4r
   ...| msgb4 , refl , refl
      with ¬cheatForgeNew {st = pre} (step-cheat x) refl unit hpk msgb4
                          (0<rnd⇒¬BootStrap v4r 0<r)
   ...| mwsb4 = voteForRound-RC-mws {vabs = vabs} hpk preReach (step-cheat x) v4r mwsb4 0<r

   open _α-Sent_
   open _BlockDataInjectivityProps_

   Abs2ImplCollision : ∀ {ab1 ab2 : Abs.Block}{post}
                     → (rPost : ReachableSystemState post)
                     → InSys (intSystemState post) (Abs.B ab1)
                     → InSys (intSystemState post) (Abs.B ab2)
                     → ab1 ≢ ab2
                     → Abs.bId ab1 ≡ Abs.bId ab2
                     → HashCollisionFound rPost
   Abs2ImplCollision rPost (ws ep≡1 m1∈pool (b∈NM {cb1} {pm1} refl refl bidcorr1))
                           (ws ep≡2 m2∈pool (b∈NM {cb2} {pm2} refl refl bidcorr2)) neq absIds≡ =
     msgmsgHC {r = rPost} (inP m1∈pool (inPM (inB {b = cb1}))) (inP m2∈pool (inPM (inB {b = cb2}))) hashes≡ bsls≢
     where
       -- TODO-2: Some of the properties should be factored out for reuse, maybe into Common?
       bIds≡ : _
       bIds≡ = trans (trans (α-Block-bid≡ cb1) absIds≡) (sym (α-Block-bid≡ cb2))

       hashes≡ : _
       hashes≡ = trans (trans bidcorr1 bIds≡) (sym bidcorr2)

       rnds≡ : ∀ {cb1 cb2} → (cb1 ^∙ bBlockData) BlockDataInjectivityProps (cb2 ^∙ bBlockData)
               → Abs.bRound (α-Block cb1) ≡ Abs.bRound (α-Block cb2)
       rnds≡ {cb1} {cb2} injprops = trans (sym (α-Block-rnd≡ cb1)) (trans (bdInjRound injprops) (α-Block-rnd≡ cb2))

       propBlock : ∀ {cb pm} → pm ^∙ pmProposal ≡ cb
                   → cb ^∙ bId ≡ pm ^∙ pmProposal ∙ bId
       propBlock refl = refl

       prevQCs≡ : ∀ {cb1 cb2}
                  → (cb1 ^∙ bBlockData) BlockDataInjectivityProps (cb2 ^∙ bBlockData)
                  → Abs.bPrevQC (α-Block cb1) ≡ Abs.bPrevQC (α-Block cb2)
       prevQCs≡ {cb1} {cb2} injprops
          with cb1 ^∙ bBlockData ∙ bdBlockType | inspect
               (cb1 ^∙_) (bBlockData ∙ bdBlockType)
       ...| Genesis      | [ R ] rewrite R                    = sym (α-Block-prevqc≡-Gen  {cb2} (bdInjBTGen injprops R))
       ...| Proposal _ _ | [ R ] rewrite R | bdInjVD injprops = sym (α-Block-prevqc≡-Prop {cb2} (trans (sym $ bdInjBTProp injprops R) R))
       ...| NilBlock     | [ R ] rewrite R | bdInjBTNil injprops R | bdInjVD injprops = refl

       bsls≢ : _
       bsls≢ _
          with hashBD-inj hashes≡
       ...| injprops = neq (Abs.Block-η
                              (rnds≡ {cb1} {cb2} injprops)
                              absIds≡
                              (prevQCs≡ {cb1} {cb2} injprops))

   Cand-3-chain-vote-b4 : ∀ {pk vabs}{pre : SystemState}{pid st' outs sp}
                          → Meta-Honest-PK pk
                          → ReachableSystemState pre
                          → let post = StepPeer-post {pid}{st'}{outs}{pre} sp in
                            (c2 : Cand-3-chain-vote (intSystemState post) vabs)
                            → (v4r : VoteForRound∈ pk (abs-vRound vabs) (epoch 𝓔) (abs-vBlockUID vabs) (msgPool pre))
                            → Σ (Cand-3-chain-vote (intSystemState pre) vabs)
                                 λ c2' → Cand-3-chain-head-round (intSystemState post) c2
                                       ≡ Cand-3-chain-head-round (intSystemState pre ) c2'
   Cand-3-chain-vote-b4 {pk} {vabs} {pre} {pid} {st'} {outs} {sp} pkH r
                        c3@(mkCand3chainvote (mkVE veBlock refl refl) c3Blk∈sys₁ qc₁ qc←b₁ rc₁ rc∈sys₁ n₁ is-2chain₁) v4r
      with v-cand-3-chain⇒0<roundv  (intSystemState $ StepPeer-post {pid}{st'}{outs}{pre} sp)
   ...| 0<r
      with voteForRound-RC {vabs = vabs} pkH r v4r (0<r c3)
   ...| b , refl , rcb , ais
      with veBlock Abs.≟Block b
   ...| no   neq = ⊥-elim (meta-no-collision-in-sys postR hcf)
        where
          post    = StepPeer-post sp
          theStep = step-peer sp
          postR   = step-s r theStep
          hcf = Abs2ImplCollision postR c3Blk∈sys₁ (InSys.stable iiah theStep (ais here)) neq refl
   ...| yes refl
      with RecordChain-irrelevant rcb (step rc₁ qc←b₁)
   ...| inj₁ (((b1 , b2) , neq , absIds≡) , b1∈rcb , b2∈rc1ext) = ⊥-elim (meta-no-collision-in-sys postR (hcf b2∈rc1ext))
      where
         post    = StepPeer-post sp
         theStep = step-peer sp
         postR   = step-s r theStep

         inSys1  = InSys.stable iiah theStep $ ais b1∈rcb
         inSys2 : _ → _
         inSys2 here = c3Blk∈sys₁
         inSys2 (there .qc←b₁ b2∈rc1ext) = rc∈sys₁ b2∈rc1ext

         hcf : _ → _
         hcf b2∈rc1ext = Abs2ImplCollision postR inSys1 (inSys2 b2∈rc1ext) neq absIds≡
   ...| inj₂ (eq-step {r₀ = .(Abs.B b)} {r₁ = .(Abs.B b)} rc0 rc1 b≈b
                      ext0@(Ext.I←B _ prevNothing)
                      ext1@(Ext.Q←B _ prevJust)
                      rcrest≈) = absurd just _ ≡ nothing case trans prevJust prevNothing of λ ()
   ...| inj₂ (eq-step {r₀ = .(Abs.B b)} {r₁ = .(Abs.B b)} rc0 rc1 b≈b
                      ext0@(Ext.Q←B {qc0} {.b} _ _)
                      ext1@(Ext.Q←B {qc1} {.b} _ _) rcrest≈) = newc3 , rnds≡
          where

            newc3 = mkCand3chainvote (mkVE b refl refl)
                                     (ais here)
                                     qc0
                                     ext0
                                     rc0
                                     (ais ∘ (_∈RC-simple_.there ext0))
                                     n₁
                                     (transp-𝕂-chain (≈RC-sym rcrest≈) is-2chain₁)
            rnds≡ = cong Abs.bRound $ kchainBlock-≈RC is-2chain₁ (suc zero) (≈RC-sym rcrest≈)

   PreferredRoundProof :
      ∀ {pk round₁ round₂ bId₁ bId₂ v₁abs v₂abs mbr} {st : SystemState}
      → ReachableSystemState st
      → Meta-Honest-PK pk
      → (v₁ : VoteForRound∈ pk round₁ (epoch 𝓔) bId₁ (msgPool st))
      → (v₂ : VoteForRound∈ pk round₂ (epoch 𝓔) bId₂ (msgPool st))
      → round₁ < round₂
      → α-ValidVote 𝓔 (msgVote v₁) mbr ≡ v₁abs
      → α-ValidVote 𝓔 (msgVote v₂) mbr ≡ v₂abs
      → (c3 : Cand-3-chain-vote (intSystemState st) v₁abs)
      → Σ (VoteParentData (intSystemState st) v₂abs)
            (λ vp → Cand-3-chain-head-round (intSystemState st) c3 ≤ Abs.round (vpParent vp))
   PreferredRoundProof {pk}{round₁}{round₂}{bId₁}{bId₂}{v₁abs}{v₂abs}{mbr}{st = post}
                       step@(step-s {pre = pre} r theStep) pkH v₁ v₂ r₁<r₂ refl refl c3
      with msgRound≡ v₁ | msgEpoch≡ v₁ | msgBId≡ v₁
         | msgRound≡ v₂ | msgEpoch≡ v₂ | msgBId≡ v₂
   ...| refl | refl | refl | refl | refl | refl
      with Impl-∈BI? (_vSignature (msgVote v₁)) | Impl-∈BI? (_vSignature (msgVote v₂))
   ...| yes init₁  | yes init₂  = let r₁≡0 = Impl-bsvr (msgSigned v₁) init₁
                                      r₂≡0 = Impl-bsvr (msgSigned v₂) init₂
                                  in ⊥-elim (<⇒≢ r₁<r₂ (trans r₁≡0 (sym r₂≡0)))
   ...| yes init₁  | no  ¬init₂ = let 0≡rv = sym (Impl-bsvr (msgSigned v₁) init₁)
                                      0<rv = v-cand-3-chain⇒0<roundv (intSystemState post) c3
                                  in ⊥-elim (<⇒≢ 0<rv 0≡rv)
   ...| no  ¬init₁ | yes init₂  = let 0≡r₂ = sym (Impl-bsvr (msgSigned v₂) init₂)
                                      r₁   = msgVote v₁ ^∙ vRound
                                  in ⊥-elim (<⇒≱ r₁<r₂ (subst (r₁ ≥_) 0≡r₂ z≤n))
   ...| no  ¬init₁ | no ¬init₂
      with theStep
   ...| step-peer {pid} {st'} {outs} cheat@(step-cheat c) = vpdPres
      where
              m₁sb4 = ¬cheatForgeNewSig r cheat unit pkH (msgSigned v₁) (msg⊆ v₁) (msg∈pool v₁) ¬init₁
              m₂sb4 = ¬cheatForgeNewSig r cheat unit pkH (msgSigned v₂) (msg⊆ v₂) (msg∈pool v₂) ¬init₂
              v₁sb4 = msgSentB4⇒VoteRound∈ (msgSigned v₁) m₁sb4
              v₂sb4 = msgSentB4⇒VoteRound∈ (msgSigned v₂) m₂sb4
              v₁abs' = α-ValidVote-trans {pk} {mbr} {pool = msgPool pre} (msgVote v₁) refl (proj₁ v₁sb4)
              v₂abs' = α-ValidVote-trans {pk} {mbr} {pool = msgPool pre} (msgVote v₂) refl (proj₁ v₂sb4)

              vpdPres : Σ (VoteParentData (intSystemState post) v₂abs)
                          (λ vp → Cand-3-chain-head-round (intSystemState post) c3 ≤ Abs.round (vpParent vp))
              vpdPres
                 with Cand-3-chain-vote-b4 {sp = step-cheat c} pkH r c3 (proj₁ v₁sb4)
              ...| c2' , c2'rnd≡
                 with PreferredRoundProof r pkH (proj₁ v₁sb4) (proj₁ v₂sb4) r₁<r₂ v₁abs' v₂abs' c2'
              ...| vpd , rnd≤
                 with stepPreservesVoteParentData theStep vpd
              ...| res , rnds≡ rewrite sym rnds≡ = res , ≤-trans (≤-reflexive c2'rnd≡) rnd≤
   ...| step-peer (step-honest stP)
      with ⊎-map₂ (msgSentB4⇒VoteRound∈ (msgSigned v₁))
                  (newMsg⊎msgSentB4 r stP pkH (msgSigned v₁) ¬init₁  (msg⊆ v₁) (msg∈pool v₁))
         | ⊎-map₂ (msgSentB4⇒VoteRound∈ (msgSigned v₂))
                  (newMsg⊎msgSentB4 r stP pkH (msgSigned v₂) ¬init₂ (msg⊆ v₂) (msg∈pool v₂))
   ...| inj₂ (v₁sb4 , refl) | inj₂ (v₂sb4 , refl)
        = vpdPres
          where
            v₁abs' = α-ValidVote-trans (msgVote v₁) refl v₁sb4
            v₂abs' = α-ValidVote-trans (msgVote v₂) refl v₂sb4

            vpdPres : _
            vpdPres
               with Cand-3-chain-vote-b4 {sp = step-honest stP} pkH r c3 v₁sb4
            ...| c2' , c2'rnd≡
               with PreferredRoundProof r pkH v₁sb4 v₂sb4 r₁<r₂ v₁abs' v₂abs' c2'
            ...| vpd , rnd≤
               with stepPreservesVoteParentData theStep vpd
            ...| res , pars≡ rewrite sym pars≡ =  res , ≤-trans (≤-reflexive c2'rnd≡) rnd≤
   ...| inj₁ (m₁∈outs , v₁pk , newV₁) | inj₁ (m₂∈outs , v₂pk , newV₂) =
              Impl-PR2 r stP pkH (msg⊆ v₁) m₁∈outs (msgSigned v₁) ¬init₁ newV₁ v₁pk (msg⊆ v₂)
                                           m₂∈outs (msgSigned v₂) ¬init₂ newV₂ v₂pk refl r₁<r₂ refl refl c3

   ...| inj₁ (m₁∈outs , v₁pk , v₁New) | inj₂ (v₂sb4 , refl) = help
        where
          round≡ = trans (msgRound≡ v₂sb4) (msgRound≡ v₂)
          ¬bootstrapV₂ = ¬Bootstrap∧Round≡⇒¬Bootstrap step pkH v₂ ¬init₂ (msgSigned v₂sb4) round≡
          epoch≡ = sym (msgEpoch≡ v₂sb4)

          implir0 : _
          implir0 = Impl-IRO r stP pkH (msg⊆ v₁) m₁∈outs (msgSigned v₁) ¬init₁ v₁New v₁pk (msg⊆ v₂sb4)
                                       (msg∈pool v₂sb4)  (msgSigned v₂sb4) ¬bootstrapV₂ epoch≡

          help : _
          help = either (λ r₂<r₁ → ⊥-elim (<⇒≯ r₁<r₂ (<-transʳ (≡⇒≤ (sym round≡)) r₂<r₁)))
                        (λ v₁sb4 → let v₁abs = α-ValidVote-trans (msgVote v₁) refl v₁sb4
                                       v₂abs = α-ValidVote-trans (msgVote v₂) refl v₂sb4
                                       c2'p  = Cand-3-chain-vote-b4 {sp = step-honest stP} pkH r c3 v₁sb4
                                       prp   = PreferredRoundProof r pkH v₁sb4 v₂sb4 r₁<r₂ v₁abs v₂abs (proj₁ c2'p)
                                       vpd'  = stepPreservesVoteParentData theStep (proj₁ prp)
                                   in (proj₁ vpd') , (≤-trans (≤-reflexive (proj₂ c2'p)) (proj₂ prp)))
                        implir0
   ...| inj₂ (v₁sb4 , refl)           | inj₁ (m₂∈outs , v₂pk , v₂New) = help
        where
          rv₁<r₂ = <-transʳ (≡⇒≤ (msgRound≡ v₁sb4)) r₁<r₂
          round≡ = trans (msgRound≡ v₁sb4) (msgRound≡ v₁)
          ¬bootstrapV₁ = ¬Bootstrap∧Round≡⇒¬Bootstrap step pkH v₁ ¬init₁ (msgSigned v₁sb4) round≡
          v₁abs' = α-ValidVote-trans (msgVote v₁) refl v₁sb4

          c2'p   = Cand-3-chain-vote-b4 {sp = step-honest stP} pkH r c3 v₁sb4

          implir1 : _
          implir1 = Impl-PR1 r stP pkH (msg⊆ v₂) m₂∈outs (msgSigned v₂) ¬init₂ v₂New v₂pk
                                   (msg⊆ v₁sb4) (msg∈pool v₁sb4) (msgSigned v₁sb4) ¬bootstrapV₁
                                   (msgEpoch≡ v₁sb4) rv₁<r₂ v₁abs' refl c3

          help : _
          help = either id
                        (λ v₂sb4 → let v₂abs' = α-ValidVote-trans (msgVote v₂) refl v₂sb4
                                       prp    = PreferredRoundProof r pkH v₁sb4 v₂sb4 r₁<r₂ v₁abs' v₂abs' (proj₁ c2'p)
                                       vpd'   = stepPreservesVoteParentData theStep (proj₁ prp)
                                   in (proj₁ vpd') , (≤-trans (≤-reflexive (proj₂ c2'p)) (proj₂ prp)))
                        implir1

   prr : Type (intSystemState st)
   prr honα refl sv refl sv' c2 round<
     with vmsg≈v (vmFor sv) | vmsg≈v (vmFor sv')
   ...| refl | refl
       = let v₁ = mkVoteForRound∈ (nm (vmFor sv)) (cv ((vmFor sv))) (cv∈nm (vmFor sv))
                                  (vmSender sv) (nmSentByAuth sv) (vmsgSigned (vmFor sv))
                                  (vmsgEpoch (vmFor sv)) refl refl
             v₂ = mkVoteForRound∈ (nm (vmFor sv')) (cv (vmFor sv')) (cv∈nm (vmFor sv'))
                                  (vmSender sv') (nmSentByAuth sv') (vmsgSigned (vmFor sv'))
                                  (vmsgEpoch (vmFor sv')) refl refl
         in PreferredRoundProof r honα v₁ v₂ round< refl refl c2


text:
module NativeInt where

open import Data.Integer.Base hiding (_+_)

postulate
  Int : Set
  toInt : ℤ -> Int
  fromInt : Int -> ℤ

{-# COMPILE GHC Int = type Int #-}
{-# COMPILE GHC toInt fromInteger #-}
{-# COMPILE GHC fromInt toInteger #-}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Numeral.Natural.Oper.FlooredDivision.Proofs.DivisibilityWithRemainder where

open import Data
open import Functional
open import Numeral.Finite
import      Numeral.Finite.Proofs as 𝕟
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.FlooredDivision.Proofs
open import Numeral.Natural.Relation.DivisibilityWithRemainder hiding (base₀ ; base₊ ; step)
open import Numeral.Natural.Relation.DivisibilityWithRemainder.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Syntax.Transitivity

-- The quotient of the divisibility relation is given by the floored division operation.
[⌊/⌋][∣ᵣₑₘ]-quotient-equality : ∀{x y r}{p : (𝐒(y) ∣ᵣₑₘ x)(r)} → ((x ⌊/⌋ 𝐒(y)) ≡ [∣ᵣₑₘ]-quotient p)
[⌊/⌋][∣ᵣₑₘ]-quotient-equality {𝟎}             {_}   {𝟎}   {DivRem𝟎} = [≡]-intro
[⌊/⌋][∣ᵣₑₘ]-quotient-equality {𝐒 .(𝕟-to-ℕ r)} {𝐒 y} {𝐒 r} {DivRem𝟎} =
  ([ 0 , 𝐒(y) ] (𝕟-to-ℕ r) div y) 🝖[ _≡_ ]-[ inddiv-smaller(𝕟.bounded{y}{r}) ]
  𝟎                               🝖-end
[⌊/⌋][∣ᵣₑₘ]-quotient-equality {𝐒 x} {𝟎} {𝟎} {DivRem𝐒 p} = [≡]-with(𝐒) $
  ([ 0 , 0 ] x div 0) 🝖[ _≡_ ]-[ [⌊/⌋]-of-1ᵣ ]
  x                   🝖[ _≡_ ]-[ [∣ᵣₑₘ]-quotient-of-1 p ]-sym
  [∣ᵣₑₘ]-quotient p   🝖-end
{-# CATCHALL #-}
[⌊/⌋][∣ᵣₑₘ]-quotient-equality {𝐒 .(x + y)} {y} {r} {DivRem𝐒 {x = x} p} =
  ([ 0 , (y) ] (𝐒(x) + y) div y) 🝖[ _≡_ ]-[ inddiv-step-denominator{0}{(y)}{𝐒(x)}{y} ]
  ([ 0 , (y) ] 𝐒(x) div 𝟎)       🝖[ _≡_ ]-[]
  𝐒([ 0 , y ] x div y)           🝖[ _≡_ ]-[ [≡]-with(𝐒) ([⌊/⌋][∣ᵣₑₘ]-quotient-equality {p = p}) ]
  𝐒([∣ᵣₑₘ]-quotient p)           🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Miscellaneous.HeterogenousId where

import      Lvl
open import Logic
open import Logic.Propositional
open import Functional
open import Type

-- TODO: Will this work for getting function extensionality? Probably not?
data IdFn {ℓ} : ∀{T : Type{ℓ}} → T → T → Stmt{Lvl.𝐒(ℓ)} where
  IdFn-intro : ∀{T}{x : T} → (IdFn x x)
  IdFn-func : ∀{A B : Type{ℓ}}{f g : A → B} → (∀{x : A} → IdFn(f(x))(g(x))) → (IdFn f g)


text:
-- The part up to "data D" could be replaced by "open import
-- Common.Prelude", but at the time of writing that seems to slow down
-- the test by something like a factor of two or three (for the GHC
-- backend, on one system).

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

data D : Set where
  @0 c : D

f : @0 D → String
f c = "Success\n"

main : IO ⊤
main = putStr (f c)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Function setoids and related constructions
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Function.Equality where

import Function as Fun
open import Level
open import Relation.Binary using (Setoid)
open import Relation.Binary.Indexed.Heterogeneous
  using (IndexedSetoid; _=[_]⇒_)
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
  as Trivial

------------------------------------------------------------------------
-- Functions which preserve equality

record Π {f₁ f₂ t₁ t₂}
         (From : Setoid f₁ f₂)
         (To : IndexedSetoid (Setoid.Carrier From) t₁ t₂) :
         Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : (x : Setoid.Carrier From) → IndexedSetoid.Carrier To x
    cong  : Setoid._≈_ From =[ _⟨$⟩_ ]⇒ IndexedSetoid._≈_ To

open Π public

infixr 0 _⟶_

_⟶_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Set _
From ⟶ To = Π From (Trivial.indexedSetoid To)

------------------------------------------------------------------------
-- Identity and composition.

id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶ A
id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }

infixr 9 _∘_

_∘_ : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
        {b₁ b₂} {B : Setoid b₁ b₂}
        {c₁ c₂} {C : Setoid c₁ c₂} →
      B ⟶ C → A ⟶ B → A ⟶ C
f ∘ g = record
  { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
  ; cong  = Fun._∘_ (cong  f) (cong  g)
  }

-- Constant equality-preserving function.

const : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
          {b₁ b₂} {B : Setoid b₁ b₂} →
        Setoid.Carrier B → A ⟶ B
const {B = B} b = record
  { _⟨$⟩_ = Fun.const b
  ; cong  = Fun.const (Setoid.refl B)
  }

------------------------------------------------------------------------
-- Function setoids

-- Dependent.

setoid : ∀ {f₁ f₂ t₁ t₂}
         (From : Setoid f₁ f₂) →
         IndexedSetoid (Setoid.Carrier From) t₁ t₂ →
         Setoid _ _
setoid From To = record
  { Carrier       = Π From To
  ; _≈_           = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
  ; isEquivalence = record
    { refl  = λ {f} → cong f
    ; sym   = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
    ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
    }
  }
  where
  open module From = Setoid From using () renaming (_≈_ to _≈₁_)
  open module To = IndexedSetoid To   using () renaming (_≈_ to _≈₂_)

-- Non-dependent.

infixr 0 _⇨_

_⇨_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Setoid _ _
From ⇨ To = setoid From (Trivial.indexedSetoid To)

-- A variant of setoid which uses the propositional equality setoid
-- for the domain, and a more convenient definition of _≈_.

≡-setoid : ∀ {f t₁ t₂} (From : Set f) → IndexedSetoid From t₁ t₂ → Setoid _ _
≡-setoid From To = record
  { Carrier       = (x : From) → Carrier x
  ; _≈_           = λ f g → ∀ x → f x ≈ g x
  ; isEquivalence = record
    { refl  = λ {f} x → refl
    ; sym   = λ f∼g x → sym (f∼g x)
    ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
    }
  } where open IndexedSetoid To

-- Parameter swapping function.

flip : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
         {b₁ b₂} {B : Setoid b₁ b₂}
         {c₁ c₂} {C : Setoid c₁ c₂} →
       A ⟶ B ⇨ C → B ⟶ A ⇨ C
flip {B = B} f = record
  { _⟨$⟩_ = λ b → record
    { _⟨$⟩_ = λ a → f ⟨$⟩ a ⟨$⟩ b
    ; cong  = λ a₁≈a₂ → cong f a₁≈a₂ (Setoid.refl B) }
  ; cong  = λ b₁≈b₂ a₁≈a₂ → cong f a₁≈a₂ b₁≈b₂
  }


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Prelude hiding (⊤)

module Control.Monad.Free.State {ℓ} (S : Type ℓ) (isSetS : isSet S) where

open import Control.Monad.Free.Quotiented
open import Data.Unit.UniversePolymorphic
open import Algebra
open import Data.List
open import Data.List.Syntax

data StateF (A : Type ℓ) : Type ℓ where
  getF : (k : S → A) → StateF A
  putF : (s : S) (k : A) → StateF A

module Laws where
  open RawMonadSyntax
  put : S → Syntax StateF ⊤
  put x = lift (putF x _)

  get : Syntax StateF S
  get = lift (getF id)

  law₁ law₂ law₃ law₄ : Law StateF

  law₁ .Γ = S × S

  law₁ .ν = ⊤
  law₁ .eqn (u , u′) .lhs = do put u
                               put u′
  law₁ .eqn (u , u′) .rhs = put u′

  law₂ .Γ = S
  law₂ .ν = S
  law₂ .eqn u .lhs = do put u
                        u′ ← get
                        return u′
  law₂ .eqn u .rhs = do put u
                        return u

  law₃ .Γ = ⊤
  law₃ .ν = S × S
  law₃ .eqn _ .lhs = do s  ← get
                        s′ ← get
                        return (s , s′)
  law₃ .eqn _ .rhs = do s ← get
                        return (s , s)

  law₄ .Γ = ⊤
  law₄ .ν = ⊤
  law₄ .eqn _ .lhs = do s ← get
                        put s
  law₄ .eqn _ .rhs = return tt

  StateLaws : Theory StateF
  StateLaws = [ law₁ , law₂ , law₃ , law₄ ]

open Laws using (StateLaws)

State : Type ℓ → Type _
State = Free StateF StateLaws

get : State S
get = lift (getF id)

put : S → State ⊤
put x = lift (putF x _)

state-alg : Φ[ StateF ⋆ A / StateLaws ] ⇒ (S → A × S)
state-alg .fst (liftF (getF k)) s = k s , s
state-alg .fst (liftF (putF s₂ k)) s₁ = k , s₂
state-alg .fst (returnF x) s = x , s
state-alg .fst (bindF _ P⟨xs⟩ _ P⟨∘k⟩) s = uncurry P⟨∘k⟩ (P⟨xs⟩ s)
state-alg .snd .c->>=idˡ f Pf x = refl
state-alg .snd .c->>=idʳ x Px = refl
state-alg .snd .c->>=assoc xs Pxs f Pf g Pg = refl
state-alg .snd .c-quot (0 , p) γ = refl
state-alg .snd .c-quot (1 , p) γ = refl
state-alg .snd .c-quot (2 , p) γ = refl
state-alg .snd .c-quot (3 , p) γ = refl

runState : State A → S → A × S
runState = ⟦ state-alg ⟧

open FreeMonadSyntax

fromState : (S → A × S) → State A
fromState k = do
  s₁ ← get
  let x , s₂ = k s₁
  put s₂
  return x

open import HITs.PropositionalTruncation
open import Relation.Binary.Equivalence.PropHIT
open import Path.Reasoning

state-state : isSet A → State A ⇔ (S → A × S)
state-state _ .fun = runState
state-state _ .inv = fromState
state-state _ .rightInv _ = refl
state-state isSetA .leftInv xs = ⟦ lemma ⟧ xs
  where
  dup : S → S × S
  dup x = x , x

  lemma : Ψ[ xs ⦂ StateF ⋆ * / StateLaws ] ⇒ (fromState (runState xs) ≡ xs)
  lemma .snd = prop-coh λ _ → uip _ _

  lemma .fst (liftF (getF k)) =
    fromState (runState (lift (getF k))) ≡⟨ {!!} ⟩
    lift (getF k) ∎

  lemma .fst (liftF (putF s k)) =
    fromState (runState (lift (putF s k))) ≡⟨ {!!} ⟩
    lift (putF s k) ∎

  lemma .fst (returnF x) =
    fromState (runState (return x)) ≡⟨⟩
    fromState (λ s → x , s) ≡⟨⟩
    (get >>= λ s → put s >> return x) ≡˘⟨ >>=-assoc get put (const (return x)) ⟩
    ((get >>= put) >> return x) ≡⟨ cong (_>> return x) (quot (3 , _) tt) ⟩
    (return tt >> return x) ≡⟨ >>=-idˡ (const (return x)) tt ⟩
    return x ∎

  lemma .fst (bindF xs P⟨xs⟩ k P⟨∘k⟩) =
    fromState (runState (xs >>= k)) ≡⟨⟩
    fromState (λ s → uncurry (runState ∘ k) (runState xs s)) ≡⟨⟩
    (get >>= λ s₁ → let x , s₂ = uncurry (runState ∘ k) (runState xs s₁) in put s₂ >> return x) ≡⟨⟩
    (get >>= λ s₁ → let x , s₂ = runState xs s₁ ; y , s₃ = runState (k x) s₂ in put s₃ >> return y) ≡⟨ {!!} ⟩
    (fromState (runState xs) >>= (fromState ∘ runState ∘ k)) ≡⟨ cong₂ Free._>>=_ P⟨xs⟩ (funExt P⟨∘k⟩) ⟩
    (xs >>= k) ∎

functorState : Functor ℓ ℓ
functorState .Functor.𝐹 = StateF
functorState .Functor.map f (getF k) = getF (f ∘ k)
functorState .Functor.map f (putF s k) = putF s (f k)
functorState .Functor.map-id i (getF k) = getF k
functorState .Functor.map-id i (putF s k) = putF s k
functorState .Functor.map-comp f g i (getF k) = getF (f ∘ g ∘ k)
functorState .Functor.map-comp f g i (putF s k) = putF s (f (g k))

-- runState′ : isSet A → State A → S → A × S
-- runState′ isSetA = cata functorState (isSetState isSetA) _,_ ϕ ℒ
--   where
--   ϕ : StateF (S → A × S) → S → A × S
--   ϕ (getF k) s = k s s
--   ϕ (putF s₂ k) s₁ = k s₂

--   ℒ : InTheory functorState {𝒯 = StateLaws} (isSetState isSetA) ϕ
--   ℒ (0 , p) f iss e = refl
--   ℒ (1 , p) f iss e = refl
--   ℒ (2 , p) f iss e = refl
--   ℒ (3 , p) f iss e = refl

-- -- open import Data.Nat using (_∸_)

-- -- example : State ℕ ℕ
-- -- example = do
-- --   x ← get
-- --   put (suc x)
-- --   put x
-- --   return (x ∸ 1)

-- -- res : ℕ × ℕ
-- -- res = runState example 5

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module my-list where

open import level
open import bool
open import eq
open import maybe
open import nat
open import nat-thms
open import product-thms
open import product

data 𝕃 {ℓ} (A : Set ℓ) : Set ℓ where
  [] : 𝕃 A
  _::_ : (x : A) (xs : 𝕃 A) → 𝕃 A

{-# BUILTIN LIST 𝕃 #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _::_  #-}

length : ∀{ℓ}{A : Set ℓ} → 𝕃 A → ℕ
length [] = 0
length (x :: x₁) = suc (length x₁)

_++_ : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A → 𝕃 A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

map : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → 𝕃 A → 𝕃 B
map f []        = []
map f (x :: xs) = f x :: map f xs

filter : ∀{ℓ}{A : Set ℓ} → (A → 𝔹) → 𝕃 A → 𝕃 A
filter p [] = []
filter p (x :: xs) = let r = filter p xs in
                     if p x then x :: r else r

-- remove all elements equal to the given one
remove : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l : 𝕃 A) → 𝕃 A
remove eq a l = filter (λ x → ~ (eq a x)) l

nth : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕃 A → maybe A
nth _ [] = nothing
nth 0 (x :: xs) = just x
nth (suc n) (x :: xs) = nth n xs

reverse-helper : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A → 𝕃 A
reverse-helper h [] = h
reverse-helper h (x :: xs) = reverse-helper (x :: h) xs

reverse : ∀ {ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A
reverse l = reverse-helper [] l

length-++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) →
            length (l1 ++ l2) ≡ (length l1) + (length l2)
length-++ [] l2 = refl
length-++ (x :: l1) l2 rewrite length-++ l1 l2 = refl

++-assoc : ∀{ℓ}{A : Set ℓ} (l1 l2 l3 : 𝕃 A) →
           (l1 ++ l2) ++ l3 ≡ l1 ++ (l2 ++ l3)
++-assoc [] l2 l3 = refl
++-assoc (x :: l1) l2 l3 rewrite ++-assoc l1 l2 l3 = refl

length-filter : ∀{ℓ}{A : Set ℓ}(p : A → 𝔹)(l : 𝕃 A) →
                length (filter p l) ≤ length l ≡ tt
length-filter p [] = refl
length-filter p (x :: l) with p x
...                      | tt = length-filter p l
...                      | ff = ≤-trans{length (filter p l)}
                                   (length-filter p l) (≤-suc (length l))

filter-idem : ∀{ℓ}{A : Set ℓ}(p : A → 𝔹)(l : 𝕃 A) →
              (filter p (filter p l)) ≡ (filter p l)
filter-idem p [] = refl
filter-idem p (x :: l) with keep (p x)
...                    | tt , p'
  rewrite p' | p' | filter-idem p l = refl
...                    | ff , p' rewrite p' = filter-idem p l

length-reverse-helper : ∀{ℓ}{A : Set ℓ}(h l : 𝕃 A) →
                        length (reverse-helper h l) ≡ length h + length l
length-reverse-helper h [] = sym (+0 (length h))
length-reverse-helper h (x :: l)
  rewrite length-reverse-helper (x :: h) l =
    sym (+suc (length h) (length l))

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

it : ∀ {a} {A : Set a} {{_ : A}} → A
it {{p}} = p

f : (a {b} {{c}} : Nat) → Nat
f = λ a {b} → it

g : (a b@(c , d) (e , f) : Σ Nat (λ _ → Nat)) → Nat
g = λ a b@(c , d) x@(e , _) → f (fst a) {d} {{e}}

h : ∀ {a} (b@(c , d) : Σ Nat (λ _ → Nat)) → Nat
h {a} b = g a b b

i : ∀ a b → Nat
i a b = h {a} b

{-
j : ∀ x → let (m , n) = x in m ≡ n
j x = {!!}
-}

data P (a {b} {{v}} c : Σ Nat (λ _ → Nat)) : Set where
  CON : a ≡ it → P a c

uncurry :
  {A : Set} {B : A → Set} {C : ∀ a → B a → Set} →
  ((a : A) (b : B a) → C a b) →
  ((a , b) : Σ A B)  → C a b
uncurry f = λ (a , b) → f a b

equal× : {A B : Set} (p q : Σ A (λ _ → B)) → Set
equal× = λ (a , b) (c , d) → Σ (a ≡ c) (λ _ → b ≡ d)

record WRAP : Set where
  constructor TTTTT
  field wrapped : Nat

id : WRAP → WRAP
id = λ x (let (TTTTT n) = x) → let (TTTTT n) = x in x

id' : WRAP → WRAP
id' = λ x@(TTTTT n) → x

id'' : WRAP → WRAP
id'' = λ (TTTTT n) → TTTTT n

shadowing : (p@(m , p) m@(r , s) : Σ Nat (λ _ → Nat)) →
  Σ (Σ Nat (p ≡_)) (λ _ → Σ _ (m ≡_))
shadowing = λ (_ , p) m → (p , refl) , (m , refl)

shadowing' : (x@(m , p) p@(r , s) : Σ Nat (λ _ → Nat)) → x ≡ p → m ≡ r
shadowing' _ _ refl = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda