inductive Hex.GraphIso.Nauty.Sparse.Loop.Rel {α : Type u_1} {β : Type u_2} (R : α → β → Prop) : ForInStep α → ForInStep β → Prop

Related loop steps make the same stop/continue choice.

• done {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} (h : R a b) : Rel R (ForInStep.done a) (ForInStep.done b)
• yield {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} (h : R a b) : Rel R (ForInStep.yield a) (ForInStep.yield b)

theorem Hex.GraphIso.Nauty.Sparse.Loop.list_rel {γ : Type u_1} {α : Type u_2} {β : Type u_3} (xs : List γ) (f : γ → α → Id (ForInStep α)) (g : γ → β → Id (ForInStep β)) (R : α → β → Prop) (hstep : ∀ (x : γ) (a : α) (b : β), R a b → Rel R (f x a) (g x b)) {a : α} {b : β} (h : R a b) : R (forIn xs a f) (forIn xs b g)

Pointwise related pure callbacks give related executed list loops.

theorem Hex.GraphIso.Nauty.Sparse.Loop.range_rel {α : Type u_1} {β : Type u_2} (n : Nat) (f : Nat → α → Id (ForInStep α)) (g : Nat → β → Id (ForInStep β)) (R : α → β → Prop) (hstep : ∀ (x : Nat) (a : α) (b : β), R a b → Rel R (f x a) (g x b)) {a : α} {b : β} (h : R a b) : R (forIn [:n] a f) (forIn [:n] b g)

The same relation applies to the literal bounded range loops used by refinement, including early breaks.

def Hex.GraphIso.Nauty.Sparse.Loop.Preserves {α : Type u_1} (P Q : α → Prop) : ForInStep α → Prop

A continuing callback retains the loop invariant; an early return only needs the final postcondition.

Equations

• Hex.GraphIso.Nauty.Sparse.Loop.Preserves P Q (ForInStep.yield a) = P a
• Hex.GraphIso.Nauty.Sparse.Loop.Preserves P Q (ForInStep.done a) = Q a

theorem Hex.GraphIso.Nauty.Sparse.Loop.list_congr {γ : Type u_1} {α : Type u_2} (xs : List γ) (f g : γ → α → Id (ForInStep α)) (P Q : α → Prop) (hpq : ∀ (a : α), P a → Q a) (hstep : ∀ (x : γ), x ∈ xs → ∀ (a : α), P a → f x a = g x a ∧ Preserves P Q (f x a)) {a : α} (h : P a) : forIn xs a f = forIn xs a g ∧ Q (forIn xs a f)

Callbacks need agree only on the states and inputs that can actually be visited. The final postcondition also covers early breaks.

theorem Hex.GraphIso.Nauty.Sparse.Loop.range_congr {α : Type u_1} (first last : Nat) (f g : Nat → α → Id (ForInStep α)) (P Q : α → Prop) (hpq : ∀ (a : α), P a → Q a) (hstep : ∀ (x : Nat), first ≤ x → x < last → ∀ (a : α), P a → f x a = g x a ∧ Preserves P Q (f x a)) {a : α} (h : P a) : forIn [first:last] a f = forIn [first:last] a g ∧ Q (forIn [first:last] a f)

Congruence for the literal bounded ranges used by the executable.

theorem Hex.GraphIso.Nauty.Sparse.Loop.indexed_congr {α : Type u_1} (first last : Nat) (f g : Nat → α → Id (ForInStep α)) (P : Nat → α → Prop) (Q : α → Prop) (hpq : ∀ (i : Nat) (a : α), P i a → Q a) (hstep : ∀ (i : Nat), first ≤ i → i < last → ∀ (a : α), P i a → f i a = g i a ∧ Preserves (P (i + 1)) Q (f i a)) {a : α} (h : P first a) : forIn [first:last] a f = forIn [first:last] a g ∧ Q (forIn [first:last] a f)

A literal range loop may use its current position in the invariant. This accounts for scans whose final increment reaches the exclusive end.