soft3/nox/proofs/T3.ei

ฯ€ 0.0% 351 words ยท 2 min 
-- nox/T3.ei โ€” parallel commutativity of witness traces
-- Source: nox/proofs/lean/T3_parallel_commutativity.lean
-- T3.1 (sort permutation invariant), T3.2 (multiset equiv), T3 main

import "Model.ei"

-- โ”€โ”€ PathStep: structural trace position โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

inductive PathStep : Type 0 where
  | left         : PathStep
  | right        : PathStep
  | test         : PathStep
  | yes          : PathStep
  | no           : PathStep
  | sub          : PathStep
  | continuation : PathStep
  | tag          : PathStep
  | check        : PathStep

-- โ”€โ”€ StructuralIndex (abstract) โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

axiom StructuralIndex : Type 0

-- โ”€โ”€ Perm: permutation relation over abstract traces (Nat) โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

axiom Perm : Nat -> Nat -> Type 0

-- nil case: empty traces (both 0) are trivially permutations
axiom Perm.nil : Perm 0 0

-- โ”€โ”€ sortByPath: canonical sort of a trace โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

axiom sortByPath : Nat -> Nat

-- โ”€โ”€ keyInjective: injectivity predicate for a trace โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

axiom keyInjective : Nat -> Type 0

-- โ”€โ”€ T3.1 โ€” sort is permutation-invariant โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
-- Requires mergeSort Perm case analysis โ€” stays as axiom.

axiom sort_permutation_invariant (t1 : Nat) (t2 : Nat)
    (h : Perm t1 t2)
    (uniq : keyInjective t1) :
    Eq Nat (sortByPath t1) (sortByPath t2)

-- keyInjective holds for the empty (0) trace
axiom keyInjective_nil : keyInjective 0

-- โ”€โ”€ T3.2 โ€” multiset equivalence โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
-- Both stubs reduce to 0 via empty-trace axioms; Perm.nil closes.

theorem threaded_trace_is_permutation (o : Noun) (t : Noun) (f : Nat) :
    Perm (trace_seq o t f) (trace_par o t f) := by {
  rewrite [trace_seq_empty o t f]
  rewrite [trace_par_empty o t f]
  exact Perm.nil
}

-- โ”€โ”€ keyInjective holds for stub traces โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

theorem trace_seq_key_injective (o : Noun) (t : Noun) (f : Nat) :
    keyInjective (trace_seq o t f) := by {
  rewrite [trace_seq_empty o t f]
  exact keyInjective_nil
}

-- โ”€โ”€ T3 main โ€” canonical-sorted trace equivalence โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€

theorem canonical_trace_equivalence (o : Noun) (t : Noun) (f : Nat)
    (uniq : keyInjective (trace_seq o t f)) :
    Eq Nat (sortByPath (trace_seq o t f)) (sortByPath (trace_par o t f)) := by {
  rewrite [trace_seq_empty o t f]
  rewrite [trace_par_empty o t f]
  rfl
}

Graph