GapCVP proof, part 04

def GapCVP.CNFFiniteRecordSort.sourceOrderedDistinctRecords {α : Type} [Encodable α] [DecidableEq α] (records : List α) : List α

GapCVP reduction support.

Equations

• GapCVP.CNFFiniteRecordSort.sourceOrderedDistinctRecords records = GapCVP.ThreeCNFReduction.sortedElements records.toFinset

@[simp]

theorem GapCVP.CNFFiniteRecordSort.sourceOrderedDistinctRecords_sortedElements {α : Type} [Encodable α] [DecidableEq α] (records : Finset α) : sourceOrderedDistinctRecords (ThreeCNFReduction.sortedElements records) = ThreeCNFReduction.sortedElements records

theorem GapCVP.CNFInputDependentRecordSort.sourceOrderedDistinctRecords_eq_of_nodup_pairwise {α : Type} [Encodable α] [DecidableEq α] (source candidate : List α) (hmembership : ∀ (record : α), record ∈ candidate ↔ record ∈ source) (hnodup : candidate.Nodup) (hpairwise : List.Pairwise (fun (first second : α) => Encodable.encode first ≤ Encodable.encode second) candidate) : CNFFiniteRecordSort.sourceOrderedDistinctRecords source = candidate

def GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue : List Bool → ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue [] = 0
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue (false :: remaining) = 2 * GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue remaining
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue (true :: remaining) = 2 * GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue remaining + 1

@[simp]

theorem GapCVP.CNFNaturalOrderComparator.littleEndianNaturalValue_encodeNat (number : ℕ) : littleEndianNaturalValue (Computability.encodeNat number) = number

@[irreducible]

def GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold : CNFEncodedClauseSort.EncodedWordOrdering → List Bool → List Bool → CNFEncodedClauseSort.EncodedWordOrdering

Compare two little-endian bit words, updating the order at each higher bit.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ [] [] = x✝
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ (false :: first) [] = GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ first []
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ [] (false :: second) = GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ [] second
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ (false :: first) (false :: second) = GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ first second
• GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ (true :: first) (true :: second) = GapCVP.CNFNaturalOrderComparator.littleEndianNaturalFold x✝ first second

def GapCVP.CNFNaturalOrderComparator.littleEndianNaturalOrdering (first second : List Bool) : CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.littleEndianNaturalOrdering_eq_value_order (first second : List Bool) : littleEndianNaturalOrdering first second = if littleEndianNaturalValue first < littleEndianNaturalValue second then CNFEncodedClauseSort.EncodedWordOrdering.less else if littleEndianNaturalValue second < littleEndianNaturalValue first then CNFEncodedClauseSort.EncodedWordOrdering.greater else CNFEncodedClauseSort.EncodedWordOrdering.equal

@[simp]

theorem GapCVP.CNFNaturalOrderComparator.littleEndianNaturalOrdering_encodeNat (first second : ℕ) : littleEndianNaturalOrdering (Computability.encodeNat first) (Computability.encodeNat second) = if first < second then CNFEncodedClauseSort.EncodedWordOrdering.less else if second < first then CNFEncodedClauseSort.EncodedWordOrdering.greater else CNFEncodedClauseSort.EncodedWordOrdering.equal

def GapCVP.CNFNaturalOrderComparator.delimitedNaturalPairOrdering (input : List Bool) : CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

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

def GapCVP.CNFNaturalOrderComparator.sourcePreservingDelimitedNaturalComparisonWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.delimitedNaturalPairOrdering_valid (first second suffix : List Bool) : delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = littleEndianNaturalOrdering first second

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderComparator.delimitedNaturalPairOrdering_encodeNat (first second : ℕ) (suffix : List Bool) : delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord (Computability.encodeNat first) ++ BinaryEncoding.lengthPrefixedWord (Computability.encodeNat second) ++ suffix) = if first < second then CNFEncodedClauseSort.EncodedWordOrdering.less else if second < first then CNFEncodedClauseSort.EncodedWordOrdering.greater else CNFEncodedClauseSort.EncodedWordOrdering.equal

def GapCVP.CNFNaturalOrderComparator.naturalCompareConsumeBoth (continuation : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) CNFEncodedClauseSort.DelimitedPairComparisonState) : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) CNFEncodedClauseSort.DelimitedPairComparisonState

Pop the next bit from each comparator stack before continuing.

Equations

• GapCVP.CNFNaturalOrderComparator.naturalCompareConsumeBoth continuation = GapCVP.CNFEncodedClauseSort.delimitedComparePop 5 (GapCVP.CNFEncodedClauseSort.delimitedComparePop 6 continuation)

def GapCVP.CNFNaturalOrderComparator.naturalCompareWordsStatement : Turing.TM2.Stmt (fun (x : Fin 10) => Bool) (Fin 12) CNFEncodedClauseSort.DelimitedPairComparisonState

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.CNFNaturalOrderComparator.delimitedNaturalComparisonMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFNaturalOrderComparator.naturalCompareConfiguration (phase : Fin 12) (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.delimitedNaturalComparisonMachine_init (input : List Bool) : Turing.initList delimitedNaturalComparisonMachine input = naturalCompareConfiguration 0 CNFEncodedClauseSort.EncodedWordOrdering.invalid input [] [] [] [] [] [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFNaturalOrderComparator.tacticNaturalCompareStepTac : Lean.ParserDescr

Executes the naturalCompareStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsEqualBit (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (bit : Bool) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) (bit :: secondForward) source sourcePrefix output) = some (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsLessBit (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (false :: firstForward) (true :: secondForward) source sourcePrefix output) = some (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.less input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsGreaterBit (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (true :: firstForward) (false :: secondForward) source sourcePrefix output) = some (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.greater input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsFirstEmptyFalse (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed [] (false :: secondForward) source sourcePrefix output) = some (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed [] secondForward source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsFirstEmptyTrue (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed secondForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed [] (true :: secondForward) source sourcePrefix output) = some (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.less input firstCounter firstReversed secondCounter secondReversed [] secondForward source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsSecondEmptyFalse (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (false :: firstForward) [] source sourcePrefix output) = some (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed firstForward [] source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsSecondEmptyTrue (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed firstForward source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed (true :: firstForward) [] source sourcePrefix output) = some (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.greater input firstCounter firstReversed secondCounter secondReversed firstForward [] source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsBothEmptyInvalid (input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.invalid input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output) = some (naturalCompareConfiguration 7 CNFEncodedClauseSort.EncodedWordOrdering.equal input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output)

theorem GapCVP.CNFNaturalOrderComparator.naturalCompareWordsBothEmpty (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (hvalid : outcome ≠ CNFEncodedClauseSort.EncodedWordOrdering.invalid) (input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) : delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output) = some (naturalCompareConfiguration 7 outcome input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output)

def GapCVP.CNFNaturalOrderComparator.naturalComparisonEffectiveOutcome (outcome : CNFEncodedClauseSort.EncodedWordOrdering) : CNFEncodedClauseSort.EncodedWordOrdering

Treat an uninitialized comparison result as equality.

Equations

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

noncomputable def GapCVP.CNFNaturalOrderComparator.naturalCompareWordsTrace (outcome : CNFEncodedClauseSort.EncodedWordOrdering) (first second input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed first second source sourcePrefix output) (some (naturalCompareConfiguration 7 (littleEndianNaturalFold (naturalComparisonEffectiveOutcome outcome) first second) input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output)) (first.length + second.length + 1)

Compare both encoded natural-number words and record their final order.

Equations

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

noncomputable def GapCVP.CNFNaturalOrderComparator.naturalCompareWordsTraceInitial (first second input firstCounter firstReversed secondCounter secondReversed source sourcePrefix output : List Bool) : StateTransition.EvalsToInTime delimitedNaturalComparisonMachine.step (naturalCompareConfiguration 6 CNFEncodedClauseSort.EncodedWordOrdering.invalid input firstCounter firstReversed secondCounter secondReversed first second source sourcePrefix output) (some (naturalCompareConfiguration 7 (littleEndianNaturalOrdering first second) input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output)) (first.length + second.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_missingFirst (count : ℕ) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (List.replicate count true) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_shortFirst (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (List.replicate count true ++ false :: payload) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_missingSecond (first : List Bool) (count : ℕ) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord first ++ List.replicate count true) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderTotalComparator.delimitedNaturalPairOrdering_shortSecond (first : List Bool) (count : ℕ) (payload : List Bool) (hshort : payload.length < count) : CNFNaturalOrderComparator.delimitedNaturalPairOrdering (BinaryEncoding.lengthPrefixedWord first ++ (List.replicate count true ++ false :: payload)) = CNFEncodedClauseSort.EncodedWordOrdering.invalid

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFNaturalOrderTotalComparator.sourcePreservingNaturalComparison_valid (first second suffix : List Bool) : CNFNaturalOrderComparator.sourcePreservingDelimitedNaturalComparisonWord (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) = BinaryEncoding.lengthPrefixedWord (BinaryEncoding.lengthPrefixedWord first ++ BinaryEncoding.lengthPrefixedWord second ++ suffix) ++ CNFEncodedClauseSort.encodedWordOrderingWord (CNFNaturalOrderComparator.littleEndianNaturalOrdering first second)

theorem GapCVP.CNFNaturalOrderCertifiedComparator.certifiedNatural_step_eq_old (configuration : CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.Cfg) (hphase : configuration.l ≠ some 6) : CNFNaturalOrderComparator.delimitedNaturalComparisonMachine.step configuration = CNFEncodedClauseSort.delimitedPairComparisonMachine.step configuration

Internal support shared across GapCVP continuation modules.