-
-
Save JamesGallicchio/9e5d08bce7ce4f9f563d1a9edc765d5b to your computer and use it in GitHub Desktop.
Stream fold termination MWE
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
namespace Stream | |
variable [Stream ρ τ] (s : ρ) | |
def take (s : ρ) : Nat → List τ × ρ | |
| 0 => ([], s) | |
| n+1 => | |
match next? s with | |
| none => ([], s) | |
| some (x,rest) => | |
let (L,rest) := take rest n | |
(x::L, rest) | |
def isEmpty : Bool := | |
Option.isNone (next? s) | |
def lengthBoundedBy (n : Nat) : Prop := | |
isEmpty (take s n).2 | |
def hasNext : ρ → ρ → Prop | |
:= λ s1 s2 => ∃ x, next? s1 = some ⟨x,s2⟩ | |
def isFinite : Prop := | |
∃ n, lengthBoundedBy s n | |
instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where | |
rel := λ s1 s2 => hasNext s2.val s1.val | |
wf := ⟨λ ⟨s,h⟩ => ⟨⟨s,h⟩, by | |
simp | |
cases h; case intro w h => | |
induction w generalizing s | |
case zero => | |
intro ⟨s',h'⟩ h_next | |
simp [hasNext] at h_next | |
cases h_next; case intro x h_next => | |
simp [lengthBoundedBy, isEmpty, Option.isNone, take, h_next] at h | |
case succ n ih => | |
intro ⟨s',h'⟩ h_next | |
simp [hasNext] at h_next | |
cases h_next; case intro x h_next => | |
simp [lengthBoundedBy, take, h_next] at h | |
have := ih s' h | |
exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) this | |
⟩⟩ | |
def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α | |
| ⟨l,h⟩ => | |
match h:next? l with | |
| none => acc | |
| some (x,xs) => | |
have h_next : hasNext l xs := by exists x; simp [hasNext, h] | |
mwe acc ⟨xs, by sorry⟩ | |
termination_by _ l => l | |
decreasing_by | |
trace_state | |
end Stream |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment