| /- | |
| Copyright (C) 2026 HCALC contributors | |
| SPDX-License-Identifier: AGPL-3.0-only | |
| Structural invariants for production nested `step`. | |
| -/ | |
| import Hcalc.Pipeline | |
| namespace Hcalc.Invariants | |
| open Hcalc Pipeline | |
| /-- Predicate preserved by nested `step` for all times / ε / δ. -/ | |
| def IsInvariant {n : Nat} (P : Carrier n → Prop) : Prop := | |
| ∀ (ε δ : Scalar) (t : Time) (x : Carrier n), | |
| P x → P (step (n := n) ε δ t x) | |
| theorem true_invariant {n : Nat} : IsInvariant (n := n) (fun _ => True) := by | |
| intro ε δ t x hx | |
| trivial | |
| theorem invariant_and {n : Nat} (P Q : Carrier n → Prop) | |
| (hP : IsInvariant (n := n) P) (hQ : IsInvariant (n := n) Q) : | |
| IsInvariant (n := n) (fun x => P x ∧ Q x) := by | |
| intro ε δ t x hx | |
| exact ⟨hP ε δ t x hx.1, hQ ε δ t x hx.2⟩ | |
| /-- Invariance under production defaults. -/ | |
| def IsInvariantProd {n : Nat} (P : Carrier n → Prop) : Prop := | |
| ∀ (t : Time) (x : Carrier n), P x → P (stepProd (n := n) t x) | |
| theorem invariant_implies_prod {n : Nat} (P : Carrier n → Prop) | |
| (h : IsInvariant (n := n) P) : IsInvariantProd (n := n) P := by | |
| intro t x hx | |
| exact h epsProd deltaProd t x hx | |
| end Hcalc.Invariants | |