Structural facts about GuardedPlusCal.Block's list-like interface, and the two induction principles the semantics is proved by. Purely syntactic — nothing here mentions values, memories, or the semantics, which is why it sits under Syntax/ rather than Semantics/.

Block is a non-empty list in disguise (begin ++ [last]), so it supports both a left-to-right view (cons/end, Block.cons_end_induct) and a right-to-left one (concat/end, Block.concat_end_induct). Semantics/Lemmas.lean needs both: reduction composes left to right, while concat-shaped rewrites arise from appending a terminal statement.

theorem GuardedPlusCal.Block.ext_iff {α : Bool → Type} {b : Bool} {B B' : Block α b} (h₁ : B.begin = B'.begin) (h₂ : B.last = B'.last) : B = B'

theorem GuardedPlusCal.Block.ext_iff_iff {α : Bool → Type} {b : Bool} {B B' : Block α b} : B = B' ↔ B.begin = B'.begin ∧ B.last = B'.last

theorem GuardedPlusCal.Block.foldr_cons_eq {α : Bool → Type} {b : Bool} {B : Block α b} {Ss : List (α false)} : List.foldr cons B Ss = { begin := Ss ++ B.begin, last := B.last }

theorem GuardedPlusCal.Block.prepend_nil {α : Bool → Type} {b : Bool} {B : Block α b} : prepend [] B = B

theorem GuardedPlusCal.Block.prepend_cons {α : Bool → Type} {b : Bool} {S : α false} {Ss : List (α false)} {B : Block α b} : prepend (S :: Ss) B = cons S (prepend Ss B)

Prepending peels one statement at a time into a cons — the equation an induction over the prepended list runs on.

theorem GuardedPlusCal.Block.concat_ne_end {α : Bool → Type} {b : Bool} {B : Block α false} {S S' : α b} : B.concat S ≠ «end» S'

theorem GuardedPlusCal.Block.last_end {α : Bool → Type} {b : Bool} {S : α b} : («end» S).last = S

theorem GuardedPlusCal.Block.last_cons {α : Bool → Type} {S : α false} {b : Bool} {B : Block α b} : (cons S B).last = B.last

theorem GuardedPlusCal.Block.last_concat {α : Bool → Type} {b : Bool} {S : α b} {B : Block α false} : (B.concat S).last = S

theorem GuardedPlusCal.Block.begin_end {α : Bool → Type} {b : Bool} {S : α b} : («end» S).begin = []

theorem GuardedPlusCal.Block.begin_concat {α : Bool → Type} {b : Bool} {S : α b} {B : Block α false} : (B.concat S).begin = B.toList

theorem GuardedPlusCal.Block.toList_concat {α : Bool → Type} {S : α false} {B : Block α false} : (B.concat S).toList = B.toList.concat S

theorem GuardedPlusCal.Block.toList_end {α : Bool → Type} {S : α false} : («end» S).toList = [S]

theorem GuardedPlusCal.Block.toList_cons {α : Bool → Type} {S : α false} {B : Block α false} : (cons S B).toList = S :: B.toList

theorem GuardedPlusCal.Block.concat_end {α : Bool → Type} {S : α false} {b : Bool} {S' : α b} : («end» S).concat S' = cons S («end» S')

theorem GuardedPlusCal.Block.concat_cons {α : Bool → Type} {S : α false} {B : Block α false} {b : Bool} {S' : α b} : (cons S B).concat S' = cons S (B.concat S')

@[irreducible]

def GuardedPlusCal.Block.cons_end_induct {α : Bool → Type} {motive : ⦃b : Bool⦄ → Block α b → Sort u_1} {b : Bool} (B : Block α b) («end» : {b : Bool} → (S : α b) → motive («end» S)) (cons : {b : Bool} → (S : α false) → (B : Block α b) → motive B → motive (cons S B)) : motive B

Left-to-right induction: a block is either a single (possibly terminal) statement or a non-terminal statement in front of a smaller block.

Equations

• One or more equations did not get rendered due to their size.
• GuardedPlusCal.Block.cons_end_induct { begin := [], last := S' } «end» cons = «end» S'

theorem GuardedPlusCal.Block.cast_end_eq_end_cast {α : Bool → Type} {b b' : Bool} {S : α b} (b_eq : b = b') : b_eq ▸ «end» S = «end» (b_eq ▸ S)

theorem GuardedPlusCal.Block.cast_cons_eq_cons_cast {α : Bool → Type} {b b' : Bool} {S : α false} {B : Block α b} (b_eq : b = b') : b_eq ▸ cons S B = cons S (b_eq ▸ B)

def GuardedPlusCal.Block.cons_end_induct' {α : Bool → Type} {motive : Block α false → Sort u_1} (B : Block α false) («end» : (S : α false) → motive («end» S)) (cons : (S : α false) → (B : Block α false) → motive B → motive (cons S B)) : motive B

Block.cons_end_induct specialized to non-terminal blocks, where the motive need not be index-polymorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem GuardedPlusCal.Block.concat_ofList {α : Bool → Type} {Ss : List (α false)} {S' : α false} {h : Ss ≠ []} : (ofList Ss h).concat S' = { begin := Ss, last := S' }

theorem GuardedPlusCal.Block.sizeOf_ofList {α : Bool → Type} {Ss : List (α false)} [(b : Bool) → SizeOf (α b)] {h : Ss ≠ []} : sizeOf (ofList Ss h) = 1 + sizeOf Ss.dropLast + sizeOf (Ss.getLast h)

@[irreducible]

def GuardedPlusCal.Block.concat_end_induct {α : Bool → Type} [(b : Bool) → SizeOf (α b)] {motive : Block α false → Sort u_1} (B : Block α false) («end» : (S : α false) → motive («end» S)) (concat : (S : α false) → (B : Block α false) → motive B → motive (B.concat S)) : motive B

Right-to-left induction: a block is either a single statement or a smaller block extended on the right. The counterpart of Block.cons_end_induct, needed wherever a proof peels the last statement off.

Equations

• One or more equations did not get rendered due to their size.
• GuardedPlusCal.Block.concat_end_induct { begin := [], last := S' } «end» concat = «end» S'

theorem GuardedPlusCal.Block.ofList_cons_of_non_empty {α : Bool → Type} {Ss : List (α false)} {S : α false} (h : Ss ≠ []) : ofList (S :: Ss) ⋯ = cons S (ofList Ss h)

theorem GuardedPlusCal.Block.ofList_singleton {α : Bool → Type} {S : α false} : ofList [S] ⋯ = «end» S

theorem GuardedPlusCal.Block.toList_left_inverse {α : Bool → Type} {Ss : List (α false)} (h : Ss ≠ []) : (ofList Ss h).toList = Ss

theorem GuardedPlusCal.Block.toList_non_empty {α : Bool → Type} {B : Block α false} : B.toList ≠ []

theorem GuardedPlusCal.Block.toList_right_inverse {α : Bool → Type} {B : Block α false} : ofList B.toList ⋯ = B

theorem GuardedPlusCal.Block.ofList_of_toList {α : Bool → Type} {B : Block α false} {Ss : List (α false)} (h : B.toList = Ss) : B = ofList Ss ⋯