MatchingLogic.EntryIII.AlphaFreshWitnessed

def MatchingLogic.AlphaFreshWitnessed {S : Signature} (Gamma : Set (Pattern S ℕ)) : Prop

A witness may be taken after replacing the existential by any pattern related by the repository's proof-theoretic alpha bridge.

Equations

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

theorem MatchingLogic.fvBlocked_has_alpha_fresh_witness : ∃ (x' : ℕ) (p' : Pattern WitnessCollapseSig ℕ) (y : ℕ), (Pattern.ex 1 ((Pattern.var 1).and (Pattern.var 0))).AlphaEq (Pattern.ex x' p') ∧ y ∉ p'.allVars ∧ (Pattern.ex x' p').imp (Pattern.captureAvoidingSubst x' y p') ∈ witnessCollapseTheory

The candidate from the probe has a proof-theoretic alpha-equivalent, vacuously quantified representative. Thus it is not a counterexample to the alpha-relaxed condition.

A binary-symbol countermodel. The small complexity of the distinguished existential leaves no room for a proof-theoretically equivalent vacuous copy of its body.

inductive MatchingLogic.AlphaWitnessSym : Type

The binary operation symbol used by the alpha-equivalence countermodels.

• pair : AlphaWitnessSym

@[instance_reducible]

instance MatchingLogic.instDecidableEqAlphaWitnessSym : DecidableEq AlphaWitnessSym

Equations

• MatchingLogic.instDecidableEqAlphaWitnessSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MatchingLogic.instFintypeAlphaWitnessSym : Fintype AlphaWitnessSym

Equations

• MatchingLogic.instFintypeAlphaWitnessSym = { elems := {MatchingLogic.AlphaWitnessSym.pair}, complete := MatchingLogic.instFintypeAlphaWitnessSym._proof_1 }

@[reducible, inline]

abbrev MatchingLogic.AlphaWitnessSig : Signature

The signature containing the binary alpha-witness operation.

Equations

• MatchingLogic.AlphaWitnessSig = { Sym := MatchingLogic.AlphaWitnessSym, arity := fun (x : MatchingLogic.AlphaWitnessSym) => 2 }

def MatchingLogic.pairArgs (p q : Pattern AlphaWitnessSig ℕ) : Fin 2 → Pattern AlphaWitnessSig ℕ

Public because alphaBlocked is public and unfolds through it: a private name in the type of a public declaration cannot be reached by the pin list.

Equations

• MatchingLogic.pairArgs p q ⟨0, isLt⟩ = p
• MatchingLogic.pairArgs p q ⟨1, isLt⟩ = q

@[simp]

theorem MatchingLogic.pairArgs_zero (p q : Pattern AlphaWitnessSig ℕ) : pairArgs p q 0 = p

@[simp]

theorem MatchingLogic.pairArgs_one (p q : Pattern AlphaWitnessSig ℕ) : pairArgs p q 1 = q

@[reducible, inline]

abbrev MatchingLogic.alphaWitnessModel : Model AlphaWitnessSig

The Boolean model used to witness the alpha-renaming obstruction.

Equations

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

def MatchingLogic.alphaWitnessRho : ℕ → alphaWitnessModel.carrier

The valuation that maps exactly variable zero to true.

Equations

• MatchingLogic.alphaWitnessRho n = decide (n = 0)

def MatchingLogic.alphaWitnessTheory : Set (Pattern AlphaWitnessSig ℕ)

The complete pointed theory of alphaWitnessModel at true.

Equations

• MatchingLogic.alphaWitnessTheory = MatchingLogic.pointedTheory MatchingLogic.alphaWitnessModel MatchingLogic.alphaWitnessRho true

theorem MatchingLogic.alphaWitnessTheory_isMCS : IsMCS alphaWitnessTheory

theorem MatchingLogic.alphaWitnessTheory_witnessed : Witnessed alphaWitnessTheory

def MatchingLogic.alphaBlocked : Pattern AlphaWitnessSig ℕ

The existential pattern whose binder cannot be renamed to variable zero.

Equations

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

theorem MatchingLogic.alphaBlocked_mem : alphaBlocked ∈ alphaWitnessTheory

@[reducible, inline]

abbrev MatchingLogic.alphaUnitEmptyModel : Model AlphaWitnessSig

The singleton model with an empty interpretation.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.alphaUnitFullModel : Model AlphaWitnessSig

The singleton model with a total interpretation.

Equations

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

def MatchingLogic.alphaUnitRho : ℕ → alphaUnitEmptyModel.carrier

The unique valuation into the singleton carrier.

Equations

• MatchingLogic.alphaUnitRho x✝ = ()

@[reducible, inline]

abbrev MatchingLogic.alphaFirstSelectorModel : Model AlphaWitnessSig

The Boolean model selecting the (true, false) input pair.

Equations

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

@[reducible, inline]

abbrev MatchingLogic.alphaCornerSelectorModel : Model AlphaWitnessSig

The Boolean model selecting the (false, true) input pair.

Equations

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

theorem MatchingLogic.alphaWitnessTheory_not_alphaFreshWitnessed : ¬AlphaFreshWitnessed alphaWitnessTheory

No proof-theoretic alpha variant of alphaBlocked has a fresh usable witness in the pointed binary model.

theorem MatchingLogic.witnessed_alphaFreshWitnessed_of_isMCS_counterexample : ∃ (Gamma : Set (Pattern AlphaWitnessSig ℕ)), IsMCS Gamma ∧ Witnessed Gamma ∧ ¬AlphaFreshWitnessed Gamma

Concrete MCS counterexample to the alpha-relaxed collapse.

theorem MatchingLogic.witnessed_alphaFreshWitnessed_of_isMCS_refuted : ¬∀ {Gamma : Set (Pattern AlphaWitnessSig ℕ)}, IsMCS Gamma → Witnessed Gamma → AlphaFreshWitnessed Gamma

The proposed implication is false, even with the broad proof-theoretic definition of Pattern.AlphaEq.