proof cleanup 1

IntersectMBO · Oct 5, 2023 · 9dcd467 · 9dcd467
1 parent f58c12d
commit 9dcd467
Showing 1 changed file with 9 additions and 15 deletions.
diff --git a/src/Ledger/Script.lagda b/src/Ledger/Script.lagda
@@ -113,16 +113,13 @@ module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot
                → evalTimelock (RequireAllOf ss)
       evalAny  : Any evalTimelock ss
                → evalTimelock (RequireAnyOf ss)
---      evalMOf  : ss' S.⊆ ss → All evalTimelock ss'
---             → evalTimelock (RequireMOf (length ss') ss)e
-      evalMOf  : ss' S.⊆ ss → All evalTimelock ss' → (n : ℕ) → n ≡ (length ss')
+      evalMOf  : {n : ℕ} → ss' S.⊆ ss → All evalTimelock ss' → n ≡ (length ss')
                → evalTimelock (RequireMOf n ss)
       evalSig  : x ∈ khs
                → evalTimelock (RequireSig x)
       evalTSt  : I .proj₁ ≡ just l → a ≤ l
                → evalTimelock (RequireTimeStart a)
       evalTEx  : I .proj₂ ≡ just r → r ≤ a
-             --  → evalTimelock (RequireTimeStart a) -- This is also wrong
                → evalTimelock (RequireTimeExpire a)
 \end{code}
 \caption{Timelock scripts and their evaluation}
@@ -163,9 +160,6 @@ module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot
   import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
     as HeterogeneousProperties
 
-  test : {A : Set} → {xs ys : List A} → xs S.⊆ ys → Bool
-  test h = false
-
   []⊆xs : {A : Set} → (xs : List A) → [] S.⊆ xs
   []⊆xs [] = HeterogeneousCore.[]
   []⊆xs (x ∷ xs) = x HeterogeneousCore.∷ʳ []⊆xs xs
@@ -187,9 +181,9 @@ module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot
                                          →  ¬ evalTimelock khs I (RequireMOf (suc n) xs)
                                          → evalTimelock khs I (RequireMOf (suc n) (x ∷ xs))
                                          → ⊥
-  evalTimelockHelper ¬p ¬p₁ (evalMOf {ss} {xs} x x₁ .(suc _) x₂) with subLemma x
+  evalTimelockHelper ¬p ¬p₁ (evalMOf {ss} {xs} x x₁ x₂) with subLemma x
   ... | inj₁ p = ¬p (evalTimelockHelper' x₁ p)
-  ... | inj₂ y = ¬p₁ (evalMOf y x₁ _ x₂)
+  ... | inj₂ y = ¬p₁ (evalMOf y x₁ x₂)
 
   evalTimelock? : (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot)(s : Timelock) → Dec (evalTimelock khs I s)
   evalTimelock? khs I (RequireAllOf []) = yes (evalAll [])
@@ -204,14 +198,14 @@ module _ ⦃ _ : DecEq Slot ⦄ (_≤_ : Slot → Slot → Set) (_≤ᵇ_ : Slot
   ... | no ¬p | no ¬p₁ = no (λ { (evalAny (here px)) → ¬p px ; (evalAny (there x)) → ¬p₁ (evalAny x)})
   ... | yes p | no ¬p₁ = yes (evalAny (here p))
   ... | yes p | yes p₁ = yes (evalAny (here p))
-  evalTimelock? khs I (RequireMOf zero x₁) = yes (evalMOf ([]⊆xs x₁) [] zero refl)
-  evalTimelock? khs I (RequireMOf (suc n) []) = no λ { (evalMOf HeterogeneousCore.[] x₁ .(suc n) ())}
+  evalTimelock? khs I (RequireMOf zero x₁) = yes (evalMOf ([]⊆xs x₁) [] refl)
+  evalTimelock? khs I (RequireMOf (suc n) []) = no λ { (evalMOf HeterogeneousCore.[] x₁ ())}
   evalTimelock? khs I (RequireMOf (suc n) (x ∷ xs)) with evalTimelock? khs I x | evalTimelock? khs I (RequireMOf n xs) |  evalTimelock? khs I (RequireMOf (suc n) xs)
-  ... | no ¬p | no ¬p₁ | no ¬p₂ = no (λ { (evalMOf {ss'} x (px ∷ x₁) .(suc n) refl) → ¬p₁ (evalMOf (HeterogeneousProperties.∷⁻ x) x₁ n refl)})
+  ... | no ¬p | no ¬p₁ | no ¬p₂ = no (λ { (evalMOf {ss'} x (px ∷ x₁) refl) → ¬p₁ (evalMOf (HeterogeneousProperties.∷⁻ x) x₁ refl)})
   ... | no ¬p | yes p | no ¬p₁ = no (λ x₁ → evalTimelockHelper ¬p ¬p₁ x₁)
-  ... | yes p | no ¬p | no ¬p₁ = no (λ { (evalMOf {ss'} x (px ∷ x₁) .(suc n) refl) → ¬p (evalMOf (HeterogeneousProperties.∷⁻ x) x₁ n refl)})
-  ... | yes p | yes (evalMOf {ss'} x₁ x₂ .(length ss') refl) | no ¬p = yes (evalMOf (refl HeterogeneousCore.∷ x₁) (p ∷ x₂) (suc n) refl)
-  ... | _     | _     | yes (evalMOf x₁ x₂ .(suc n) x₃) = yes (evalMOf (x HeterogeneousCore.∷ʳ x₁) x₂ (suc n) x₃)
+  ... | yes p | no ¬p | no ¬p₁ = no (λ { (evalMOf {ss'} x (px ∷ x₁) refl) → ¬p (evalMOf (HeterogeneousProperties.∷⁻ x) x₁ refl)})
+  ... | yes p | yes (evalMOf {ss'} x₁ x₂ refl) | no ¬p = yes (evalMOf (refl HeterogeneousCore.∷ x₁) (p ∷ x₂) refl)
+  ... | _     | _     | yes (evalMOf x₁ x₂ x₃) = yes (evalMOf (x HeterogeneousCore.∷ʳ x₁) x₂ x₃)
   evalTimelock? khs I (RequireSig x) with x ∈? khs
   ... | no ¬p = no λ { (evalSig x) → ¬p x}
   ... | yes p = yes (evalSig p)