diff --git a/LeanPool/GapCVP/Part01A.lean b/LeanPool/GapCVP/Part01A.lean index 61f6c5d95a..33b3cf14a8 100644 --- a/LeanPool/GapCVP/Part01A.lean +++ b/LeanPool/GapCVP/Part01A.lean @@ -7,7 +7,6 @@ Authors: OpenAI, Dean Cureton module -- shake: keep-all public import Mathlib.Algebra.Group.Translate -import Mathlib.Algebra.Module.ZLattice.Basic public import Mathlib.Algebra.Order.Ring.Star public import Mathlib.Algebra.Order.Star.Real public import Mathlib.Computability.Language @@ -201,28 +200,32 @@ private theorem isClosed_of_subset_euclidean_integer_grid (Set.range (EuclideanSpace.basisFun (Fin n) ℝ).toBasis) : Set (EuclideanSpace ℝ (Fin n)))) : IsClosed s := by + classical let b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ (Fin n)) := (EuclideanSpace.basisFun (Fin n) ℝ).toBasis - let G : Submodule ℤ (EuclideanSpace ℝ (Fin n)) := - Submodule.span ℤ (Set.range b) - have hclosed : IsClosed (G : Set (EuclideanSpace ℝ (Fin n))) := by - change IsClosed (G.toAddSubgroup : Set (EuclideanSpace ℝ (Fin n))) - exact AddSubgroup.isClosed_of_discreteTopology - have hsub' : s ⊆ (G : Set (EuclideanSpace ℝ (Fin n))) := hsub - let inside : Set G := ((↑) : G → EuclideanSpace ℝ (Fin n)) ⁻¹' s - have hinside : IsClosed inside := isClosed_discrete inside - have himage : IsClosed - (((↑) : G → EuclideanSpace ℝ (Fin n)) '' inside) := - hclosed.isClosedMap_subtype_val inside hinside - have heq : - (((↑) : G → EuclideanSpace ℝ (Fin n)) '' inside) = s := by - ext x - constructor - · rintro ⟨y, hy, rfl⟩ - exact hy - · intro hx - exact ⟨⟨x, hsub' hx⟩, hx, rfl⟩ - rwa [heq] at himage + have coordinates (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ s) (i : Fin n) : + ∃ value : ℤ, (value : ℝ) = x i := by + obtain ⟨value, equality⟩ := (b.mem_span_iff_repr_mem ℤ x).mp (hsub hx) i + refine ⟨value, ?_⟩ + exact equality + refine Metric.isClosed_of_pairwise_le_dist (show (0 : ℝ) < 1 by norm_num) ?_ + intro x hx y hy different + have differ : ∃ i, x i ≠ y i := by + by_contra equal + apply different + ext i + exact not_not.mp (not_exists.mp equal i) + obtain ⟨i, hi⟩ := differ + obtain ⟨a, ha⟩ := coordinates x hx i + obtain ⟨c, hc⟩ := coordinates y hy i + have unequal : a - c ≠ 0 := by + intro equal + exact hi (ha.symm.trans ((congrArg (fun value : ℤ => (value : ℝ)) + (sub_eq_zero.mp equal)).trans hc)) + have separated : (1 : ℝ) ≤ dist (x i) (y i) := by + rw [Real.dist_eq, ← ha, ← hc, ← Int.cast_sub, ← Int.cast_abs] + exact_mod_cast Int.one_le_abs unequal + exact separated.trans (PiLp.dist_apply_le x y i) private theorem instance_latticePoint_range_isClosed (I : GapCVPInstance) : IsClosed (Set.range I.latticePoint) := by @@ -2278,11 +2281,11 @@ private theorem symbol_unique_of_satisfiesFormula {T S : ℕ} rcases hliteral with hleft | hright · subst literal have hfalse : assignment (t, i, a) = false := by - simpa only [negative] using hvalue + exact hvalue simp only [ha, Bool.true_eq_false] at hfalse · subst literal have hfalse : assignment (t, i, b) = false := by - simpa only [negative] using hvalue + exact hvalue simp only [hb, Bool.true_eq_false] at hfalse rcases lt_trichotomy a b with hab | hab | hab · exact (exclude a b hab ha hb).elim @@ -2331,7 +2334,7 @@ private theorem traceOfAssignment_initial {T S : ℕ} simp only [initialClause, Finset.mem_singleton] at hliteral subst literal apply traceOfAssignment_eq_of_selected spec assignment hsat 0 i - simpa only [positive] using hvalue + exact hvalue private theorem traceOfAssignment_accepting {T S : ℕ} (spec : Specification T S) @@ -2349,7 +2352,7 @@ private theorem traceOfAssignment_accepting {T S : ℕ} obtain ⟨i, rfl⟩ := hliteral refine ⟨i, traceOfAssignment_eq_of_selected spec assignment hsat (Fin.last T) i spec.accept ?_⟩ - simpa only [positive] using hvalue + exact hvalue private theorem traceOfAssignment_transition {T S : ℕ} (spec : Specification T S) @@ -2382,7 +2385,7 @@ private theorem traceOfAssignment_transition {T S : ℕ} · subst literal have hfalse : assignment (w.1.1, leftPosition w, symbols.1) = false := by - simpa only [negative] using hvalue + exact hvalue have htrue := traceOfAssignment_selected spec assignment hsat w.1.1 (leftPosition w) change assignment @@ -2392,7 +2395,7 @@ private theorem traceOfAssignment_transition {T S : ℕ} simp only [htrue, Bool.true_eq_false] at hfalse · subst literal have hfalse : assignment (w.1.1, w.1.2, symbols.2.1) = false := by - simpa only [negative] using hvalue + exact hvalue have htrue := traceOfAssignment_selected spec assignment hsat w.1.1 w.1.2 change assignment @@ -2403,7 +2406,7 @@ private theorem traceOfAssignment_transition {T S : ℕ} · subst literal have hfalse : assignment (w.1.1, rightPosition w, symbols.2.2.1) = false := by - simpa only [negative] using hvalue + exact hvalue have htrue := traceOfAssignment_selected spec assignment hsat w.1.1 (rightPosition w) change assignment @@ -2414,7 +2417,7 @@ private theorem traceOfAssignment_transition {T S : ℕ} · subst literal have hfalse : assignment (nextTime w, w.1.2, symbols.2.2.2) = false := by - simpa only [negative] using hvalue + exact hvalue have htrue := traceOfAssignment_selected spec assignment hsat (nextTime w) w.1.2 change assignment @@ -3343,7 +3346,7 @@ theorem ConfigurationTrace.iterate_configuration some (trace.configuration ⟨i + 1, by omega⟩) exact trace.transition ⟨i, hilt⟩ have hi : i.val ≤ steps := by omega - simpa only [advance] using hprefix i.val hi + exact hprefix i.val hi /-- GapCVP reduction support. -/ def ConfigurationTrace.evalsToAt @@ -3420,9 +3423,9 @@ theorem evalsTo_terminal_unique_of_steps_le dsimp [extra] omega have ha_run : (advance^[ha.steps]) (some initial) = some a := by - simpa only [advance] using ha.evals_in_steps + exact ha.evals_in_steps have hb_run : (advance^[hb.steps]) (some initial) = some b := by - simpa only [advance] using hb.evals_in_steps + exact hb.evals_in_steps have hrun : (advance^[extra]) (some a) = some b := by calc (advance^[extra]) (some a) = @@ -3438,8 +3441,7 @@ theorem evalsTo_terminal_unique_of_steps_le cases he : extra with | zero => rw [he] at hrun - exact Option.some.inj (by simpa only [Option.some.injEq, Function.iterate_zero, id_eq] - using hrun) + exact Option.some.inj (by exact hrun) | succ n => have hnone : (advance^[extra]) (some a) = none := by rw [he, Function.iterate_succ_apply] @@ -4211,11 +4213,11 @@ def statementPushSources | push stack value next ih => simp only [statementPushSources, List.length_cons, ih, statementPushSlots] | peek stack value next ih => - simpa only [statementPushSources, statementPushSlots] using ih + exact ih | pop stack value next ih => - simpa only [statementPushSources, statementPushSlots] using ih + exact ih | load value next ih => - simpa only [statementPushSources, statementPushSlots] using ih + exact ih | branch test yes no ihyes ihno => simp only [statementPushSources, List.length_append, ihyes, ihno, statementPushSlots] | goto value => rfl @@ -4821,8 +4823,7 @@ theorem certificatePhase_append_old_marker (certificate : List Bool) (bit : Bool) : certificatePhase (certificate ++ [bit]) certificate.length = if bit then PhaseTag.verifying else PhaseTag.guessing := by - cases bit <;> - simp [certificatePhase] + simp [certificatePhase] theorem certificatePhase_append_new_marker (certificate : List Bool) (bit : Bool) : @@ -4883,7 +4884,7 @@ theorem guessPhaseWindow_of_append certificatePhase (certificate ++ [bit]) index.val = .guessing ∨ certificatePhase (certificate ++ [bit]) index.val = .verifying rw [hmarker, certificatePhase_append_old_marker] - cases bit <;> simp + simp · by_cases hsuccessor : index.val = certificate.length + 1 · have hleft : (leftBlock width index).val = certificate.length := by @@ -5081,7 +5082,7 @@ private theorem canonicalStackAtoms_drop SupportedStackValue machine stack candidate := by intro candidate hcandidate exact hsupported candidate (by simp only [List.mem_cons, hcandidate, or_true]) - simpa only [canonicalStackAtoms, List.pmap, List.drop_succ_cons] using ih values htail + exact ih values htail private theorem canonicalStackAtoms_congr {verifier : List Bool × List Bool → Bool} @@ -6620,7 +6621,7 @@ private theorem executePrefixScript_bounds at hnext ⊢ omega | peek stack update continuation ih => - simpa only [executePrefixScript, statementStackActions] using + exact ih (update state (scriptStacks original script stack).head?) script | pop stack update continuation ih => have hnext := ih @@ -6651,7 +6652,7 @@ private theorem executePrefixScript_bounds statementStackActions] at hnext ⊢ omega | load update continuation ih => - simpa only [executePrefixScript, statementStackActions] using ih (update state) script + exact ih (update state) script | branch test yes no ihyes ihno => cases htest : test state with | false => @@ -7733,7 +7734,7 @@ theorem configurationTrace_stackAtomSupported trace.configuration (⟨0, by omega⟩ : Fin (steps + 1)) = Turing.initList machine.tm (verifierInput machine x certificate) := by - simpa only [Fin.zero_eta] using trace.initial + exact trace.initial rw [hzero] exact initialConfiguration_stackAtomSupported machine x certificate @@ -7746,7 +7747,7 @@ theorem configurationTrace_stackAtomSupported (trace.transition ⟨time, hlt⟩) (ih hprior) intro time - simpa only [Fin.eta] using hprefix time.val (by omega) + exact hprefix time.val (by omega) theorem acceptedExecution_stack_length_le_rowWidth (bound : Polynomial ℕ) @@ -7830,4 +7831,36 @@ end CLCompleteVerifierSimulation end GapCVP +namespace GapCVP + +public meta section + +/-- Expose the selected configuration before simplifying its machine program. -/ +macro "reduceMachineConfiguration" "[" configurations:term,* "]" + "(" continuation:tactic ")" : tactic => + `(tactic| + (dsimp only [$[$configurations:term],*, Turing.haltList, Turing.FinTM2.step, + Turing.TM2.step, Turing.TM2.stepAux] <;> $continuation)) + +/-- Prove a concrete machine step using its definitions and pointwise stack equality. -/ +macro "machineStackEquality" "[" definitions:term,* "]" : tactic => + `(tactic| + (first + | rfl + | (simp only [$[$definitions:term],*, + Fin.isValue, Turing.FinTM2.step, Turing.TM2.step, ↓reduceIte, Turing.TM2.stepAux, + Matrix.cons_val_zero, List.head?_cons, Option.isSome_some, List.tail_cons, + Option.getD_some, ne_eq, not_false_eq_true, Function.update_of_ne, + Matrix.cons_val_one, Fin.reduceEq, Matrix.cons_val, cond_eq_ite, List.head?_nil, + Option.isSome_none, List.tail_nil, Option.getD_none, Bool.false_eq_true, + Turing.haltList, eq_mpr_eq_cast, cast_eq, dite_eq_ite, BEq.rfl, + Option.some_beq_some, beq_true, List.isSome_head?, ite_not, Nat.reduceEqDiff, + reduceCtorEq] <;> + try { congr 2; funext stack; fin_cases stack <;> + (first | rfl | simp [Function.update]) } <;> try rfl))) + +end + +end GapCVP + end diff --git a/LeanPool/GapCVP/Part02.lean b/LeanPool/GapCVP/Part02.lean index cf488d75b1..9fc0aa7d66 100644 --- a/LeanPool/GapCVP/Part02.lean +++ b/LeanPool/GapCVP/Part02.lean @@ -464,7 +464,7 @@ private theorem canonicalAnchoredVerifierWindow_allowed_iff have hbranch : AnchoredVerificationAllowed machine window ∨ AnchoredAcceptanceAllowed machine window := by - simpa only [hmode] using hallowed'.2 + exact hallowed'.2 rcases hbranch with hverification | hacceptance · have hverification' := hverification simp only [AnchoredVerificationAllowed, CompleteVerificationAllowed, @@ -1960,7 +1960,7 @@ private theorem initializedPhaseBlock_decodableOrBlank ((initializedPhaseBlock machine old payload range offset).2.2.1 stack) := by by_cases hrange : range offset = true - · have hrangeBool : range offset := by simpa only using hrange + · have hrangeBool : range offset := by exact hrange simp only [initializedPhaseBlock, hrangeBool, ↓reduceIte] exact initialPairedAtom_decodableOrBlank machine stack (payload offset) · have hfalse := Bool.eq_false_of_not_eq_true hrange @@ -3477,7 +3477,7 @@ private theorem finiteHeadScriptRun_eq_fullPacked (fun stack => decodedFullPackedPhaseStack machine width row stack) finite.stk (emptyPrefixScript machine.tm.Γ) - (by simpa only [scriptStacks_empty] using hlookahead) + (by exact hlookahead) change executePrefixScript (machine.tm.m label) state finite.stk (emptyPrefixScript machine.tm.Γ) = @@ -3799,8 +3799,8 @@ private theorem allCorrectedVerifierWindows_controls CLLocalWindows.leftBlock_zero, hfirst, hnext, reduceCtorEq, window] at hquery | some nextControl => refine ⟨firstControl, nextControl, ?_, ?_⟩ - · simpa only [completeMachineHead] using hfirst - · simpa only [completeMachineHead] using hnext + · exact hfirst + · exact hnext private theorem decodedFullPackedPhaseConfiguration_stack {verifier : List Bool × List Bool → Bool} @@ -5451,7 +5451,7 @@ private theorem allInitializationWindows_initialControl (first 0).rangeHead (⟨0, blockSize_pos machine.tm⟩ : Fin (blockSize machine.tm)) = true := by - simpa only [firstPhaseOffset] using hrange + exact hrange have hlabel : (initializedPhaseBlock machine (completeMachineHead machine.tm (first 0)) @@ -5879,11 +5879,11 @@ private theorem evalsTo_prefix_steps_le_terminal omega have hhaltRun : (advance^[halting.steps]) (some initial) = some terminal := by - simpa only [advance] using halting.evals_in_steps + exact halting.evals_in_steps have hprefixRun : (advance^[partialRun.steps]) (some initial) = some configuration := by - simpa only [advance] using partialRun.evals_in_steps + exact partialRun.evals_in_steps have hremaining : (advance^[extra]) (some terminal) = some configuration := by calc @@ -6677,7 +6677,7 @@ private theorem canonicalAnchoredVerifyingRow_blockAtom_decode rw [stackAtomsOfBlock_pack_canonical machine (rowWidth bound machine x) certificate configuration hsupported hspace position stack] - simpa only [atomBlockAt] using + exact paddedAtom_decode machine stack (canonicalStackAtoms_forall₂ machine stack (configuration.stk stack) (stackAtomSupported_supportedValues machine configuration hsupported stack)) diff --git a/LeanPool/GapCVP/Part03A.lean b/LeanPool/GapCVP/Part03A.lean index 9ee06b5d4f..dea3944c1b 100644 --- a/LeanPool/GapCVP/Part03A.lean +++ b/LeanPool/GapCVP/Part03A.lean @@ -755,7 +755,7 @@ private theorem paddedAcceptedExecutionNaturalRow_initializationWindows execution.certificate (execution.trace.configuration 0) (supported 0) (hint 0) false := by - simpa only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero] using + exact paddedAcceptedExecutionNaturalRow_verifying bound machine execution supported hint 0 rw [hsource, htarget] simp only [List.take_length] @@ -818,7 +818,7 @@ private theorem paddedAcceptedExecutionNaturalRow_verifierWindows (execution.trace.configuration (Fin.castSucc time)) (supported (Fin.castSucc time)) (hint (Fin.castSucc time)) false := by - simpa only [Fin.val_castSucc] using + exact paddedAcceptedExecutionNaturalRow_verifying bound machine execution supported hint (Fin.castSucc time) have htarget : @@ -829,7 +829,7 @@ private theorem paddedAcceptedExecutionNaturalRow_verifierWindows execution.certificate (execution.trace.configuration time.succ) (supported time.succ) (hint time.succ) false := by - simpa only [Nat.add_assoc, Fin.val_succ] using + exact paddedAcceptedExecutionNaturalRow_verifying bound machine execution supported hint time.succ rw [hsource, htarget] @@ -1297,6 +1297,14 @@ macro "prefixWriterStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a prefix writer step using the fixed simplification rules. -/ +macro "prefixWriterStepOnly" : tactic => + `(tactic| machineStackEquality [ + structuralPrefixWriter, prefixWriterConfiguration, prefixWriterPeek, prefixWriterPop, + prefixWriterPushBit, prefixWriterPushMarker, prefixWriterGoto, prefixWriterScanStatement, + prefixWriterRestoreStatement, prefixWriterMarkerStatement, Turing.haltList, + Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + theorem prefixWriterScanStep (bit : Bool) (input scratch markers output : List Bool) : structuralPrefixWriter.step @@ -1304,14 +1312,14 @@ theorem prefixWriterScanStep (bit : Bool) (bit :: input) scratch markers output) = some (prefixWriterConfiguration 0 input (bit :: scratch) (true :: markers) output) := by - cases bit <;> prefixWriterStepTac + prefixWriterStepOnly theorem prefixWriterScanFinish (scratch markers output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 0 [] scratch markers output) = some (prefixWriterConfiguration 1 [] scratch markers output) := by - prefixWriterStepTac + rfl theorem prefixWriterRestoreStep (bit : Bool) (scratch markers output : List Bool) : @@ -1320,7 +1328,7 @@ theorem prefixWriterRestoreStep (bit : Bool) (bit :: scratch) markers output) = some (prefixWriterConfiguration 1 [] scratch markers (bit :: output)) := by - cases bit <;> prefixWriterStepTac + prefixWriterStepOnly theorem prefixWriterRestoreFinish (markers output : List Bool) : @@ -1328,7 +1336,7 @@ theorem prefixWriterRestoreFinish (prefixWriterConfiguration 1 [] [] markers output) = some (prefixWriterConfiguration 2 [] [] markers (false :: output)) := by - prefixWriterStepTac + prefixWriterStepOnly theorem prefixWriterMarkerStep (bit : Bool) (markers output : List Bool) : @@ -1336,13 +1344,13 @@ theorem prefixWriterMarkerStep (bit : Bool) (prefixWriterConfiguration 2 [] [] (bit :: markers) output) = some (prefixWriterConfiguration 2 [] [] markers (true :: output)) := by - cases bit <;> prefixWriterStepTac + prefixWriterStepOnly theorem prefixWriterFinish (output : List Bool) : structuralPrefixWriter.step (prefixWriterConfiguration 2 [] [] [] output) = some (Turing.haltList structuralPrefixWriter output) := by - prefixWriterStepTac + prefixWriterStepOnly /-- The scan phase reverses the input onto scratch and records its length in markers. -/ def prefixWriterScanTrace @@ -1740,8 +1748,8 @@ private theorem unaryPrefixMachine_drain_step unaryPrefixMachine.step (unaryConfiguration false (bit :: input) count) = some (unaryConfiguration false input count) := by - cases bit <;> - compactMachineStepTac [unaryPrefixMachine, unaryConfiguration] + machineStackEquality [ + unaryPrefixMachine, unaryConfiguration] private theorem unaryPrefixMachine_finish_prefix (count : ℕ) : unaryPrefixMachine.step (unaryConfiguration true [] count) = @@ -1989,14 +1997,16 @@ theorem payload_prefix_true (payloadConfiguration 0 (true :: input) counter reversed output) = some (payloadConfiguration 0 input (true :: counter) reversed output) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] theorem payloadPrefixDelimiter (input counter reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 0 (false :: input) counter reversed output) = some (payloadConfiguration 1 input counter reversed output) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_prefix_missing_delimiter @@ -2004,7 +2014,7 @@ theorem payload_prefix_missing_delimiter payloadDecoderMachine.step (payloadConfiguration 0 [] counter reversed output) = some (payloadConfiguration 4 [] counter reversed output) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_copy_step @@ -2014,7 +2024,8 @@ theorem payload_copy_step (true :: counter) reversed output) = some (payloadConfiguration 1 input counter (bit :: reversed) output) := by - cases bit <;> compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_insufficient @@ -2023,7 +2034,7 @@ theorem payload_insufficient (payloadConfiguration 1 [] (true :: counter) reversed output) = some (payloadConfiguration 4 [] (true :: counter) reversed output) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_counter_complete @@ -2031,14 +2042,15 @@ theorem payload_counter_complete payloadDecoderMachine.step (payloadConfiguration 1 input [] reversed output) = some (payloadConfiguration 2 input [] reversed output) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + rfl theorem payloadReverseStep (bit : Bool) (input reversed output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 2 input [] (bit :: reversed) output) = some (payloadConfiguration 2 input [] reversed (bit :: output)) := by - cases bit <;> compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_reverse_complete @@ -2046,21 +2058,23 @@ theorem payload_reverse_complete payloadDecoderMachine.step (payloadConfiguration 2 input [] [] output) = some (payloadConfiguration 3 input [] [] output) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + rfl theorem payloadDrainStep (bit : Bool) (input output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 3 (bit :: input) [] [] output) = some (payloadConfiguration 3 input [] [] output) := by - cases bit <;> compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] theorem payloadDrainFinish (output : List Bool) : payloadDecoderMachine.step (payloadConfiguration 3 [] [] [] output) = some (Turing.haltList payloadDecoderMachine (true :: output)) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_failure_drop_input @@ -2068,7 +2082,8 @@ theorem payload_failure_drop_input payloadDecoderMachine.step (payloadConfiguration 4 (bit :: input) counter reversed output) = some (payloadConfiguration 4 input counter reversed output) := by - cases bit <;> compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_failure_drop_counter @@ -2076,7 +2091,8 @@ theorem payload_failure_drop_counter payloadDecoderMachine.step (payloadConfiguration 4 [] (bit :: counter) reversed output) = some (payloadConfiguration 4 [] counter reversed output) := by - cases bit <;> compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_failure_drop_reversed @@ -2084,7 +2100,8 @@ theorem payload_failure_drop_reversed payloadDecoderMachine.step (payloadConfiguration 4 [] [] (bit :: reversed) output) = some (payloadConfiguration 4 [] [] reversed output) := by - cases bit <;> compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem payload_failure_finish @@ -2092,7 +2109,8 @@ theorem payload_failure_finish payloadDecoderMachine.step (payloadConfiguration 4 [] [] [] output) = some (Turing.haltList payloadDecoderMachine (false :: output)) := by - compactMachineStepTac [payloadDecoderMachine, payloadConfiguration] + machineStackEquality [ + payloadDecoderMachine, payloadConfiguration] @[simp] theorem replicate_true_append_cons (count : ℕ) (tail : List Bool) : diff --git a/LeanPool/GapCVP/Part03B.lean b/LeanPool/GapCVP/Part03B.lean index 1ccd09e85e..6d0b928bfb 100644 --- a/LeanPool/GapCVP/Part03B.lean +++ b/LeanPool/GapCVP/Part03B.lean @@ -549,7 +549,8 @@ theorem suffix_prefix_true (suffixConfiguration 0 (true :: input) counter reversed output) = some (suffixConfiguration 0 input (true :: counter) reversed output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_prefix_delimiter @@ -557,7 +558,8 @@ theorem suffix_prefix_delimiter suffixDecoderMachine.step (suffixConfiguration 0 (false :: input) counter reversed output) = some (suffixConfiguration 1 input counter reversed output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_prefix_missing_delimiter @@ -565,7 +567,7 @@ theorem suffix_prefix_missing_delimiter suffixDecoderMachine.step (suffixConfiguration 0 [] counter reversed output) = some (suffixConfiguration 5 [] counter reversed output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_copy_step @@ -575,7 +577,8 @@ theorem suffix_copy_step (true :: counter) reversed output) = some (suffixConfiguration 1 input counter (bit :: reversed) output) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_insufficient @@ -584,7 +587,7 @@ theorem suffix_insufficient (suffixConfiguration 1 [] (true :: counter) reversed output) = some (suffixConfiguration 5 [] (true :: counter) reversed output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_counter_complete @@ -592,7 +595,7 @@ theorem suffix_counter_complete suffixDecoderMachine.step (suffixConfiguration 1 input [] reversed output) = some (suffixConfiguration 2 input [] reversed output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_discard_step @@ -600,7 +603,8 @@ theorem suffix_discard_step suffixDecoderMachine.step (suffixConfiguration 2 input [] (bit :: reversed) output) = some (suffixConfiguration 2 input [] reversed output) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_discard_complete @@ -608,7 +612,7 @@ theorem suffix_discard_complete suffixDecoderMachine.step (suffixConfiguration 2 input [] [] output) = some (suffixConfiguration 3 input [] [] output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_collect_step @@ -617,7 +621,8 @@ theorem suffix_collect_step (suffixConfiguration 3 (bit :: input) [] reversed output) = some (suffixConfiguration 3 input [] (bit :: reversed) output) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_collect_complete @@ -625,7 +630,7 @@ theorem suffix_collect_complete suffixDecoderMachine.step (suffixConfiguration 3 [] [] reversed output) = some (suffixConfiguration 4 [] [] reversed output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_restore_step @@ -633,7 +638,8 @@ theorem suffix_restore_step suffixDecoderMachine.step (suffixConfiguration 4 [] [] (bit :: reversed) output) = some (suffixConfiguration 4 [] [] reversed (bit :: output)) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_restore_finish @@ -641,7 +647,8 @@ theorem suffix_restore_finish suffixDecoderMachine.step (suffixConfiguration 4 [] [] [] output) = some (Turing.haltList suffixDecoderMachine output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_failure_drop_input @@ -649,7 +656,8 @@ theorem suffix_failure_drop_input suffixDecoderMachine.step (suffixConfiguration 5 (bit :: input) counter reversed output) = some (suffixConfiguration 5 input counter reversed output) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_failure_drop_counter @@ -657,7 +665,8 @@ theorem suffix_failure_drop_counter suffixDecoderMachine.step (suffixConfiguration 5 [] (bit :: counter) reversed output) = some (suffixConfiguration 5 [] counter reversed output) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_failure_drop_reversed @@ -665,7 +674,8 @@ theorem suffix_failure_drop_reversed suffixDecoderMachine.step (suffixConfiguration 5 [] [] (bit :: reversed) output) = some (suffixConfiguration 5 [] [] reversed output) := by - cases bit <;> compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem suffix_failure_finish @@ -673,7 +683,8 @@ theorem suffix_failure_finish suffixDecoderMachine.step (suffixConfiguration 5 [] [] [] output) = some (Turing.haltList suffixDecoderMachine output) := by - compactMachineStepTac [suffixDecoderMachine, suffixConfiguration] + machineStackEquality [ + suffixDecoderMachine, suffixConfiguration] end SourceFormulaStructuralDecoder diff --git a/LeanPool/GapCVP/Part03C.lean b/LeanPool/GapCVP/Part03C.lean index 39306df059..c922ed328a 100644 --- a/LeanPool/GapCVP/Part03C.lean +++ b/LeanPool/GapCVP/Part03C.lean @@ -613,8 +613,13 @@ theorem variablePrefixTrue some (variableConfiguration (variablePrefixLabel position) input (true :: counter) count) := by fin_cases position <;> - compactMachineStepTac [variableClauseMachine, variableConfiguration, variablePrefixLabel, - variablePrefixStatement] + reduceMachineConfiguration + [variableConfiguration] + (compactMachineStepTac [ + variableClauseMachine, + variableConfiguration, + variablePrefixLabel, + variablePrefixStatement]) theorem variablePrefixDelimiter (position : Fin 3) (input counter : List Bool) (count : ℕ) : @@ -624,8 +629,14 @@ theorem variablePrefixDelimiter some (variableConfiguration (variablePayloadLabel position) input counter count) := by fin_cases position <;> - compactMachineStepTac [variableClauseMachine, variableConfiguration, variablePrefixLabel, - variablePayloadLabel, variablePrefixStatement] + reduceMachineConfiguration + [variableConfiguration] + (compactMachineStepTac [ + variableClauseMachine, + variableConfiguration, + variablePrefixLabel, + variablePayloadLabel, + variablePrefixStatement]) theorem variablePayloadStep (position : Fin 3) (bit counterBit : Bool) @@ -635,9 +646,14 @@ theorem variablePayloadStep (bit :: input) (counterBit :: counter) count) = some (variableConfiguration (variablePayloadLabel position) input counter count) := by - fin_cases position <;> cases bit <;> cases counterBit <;> - compactMachineStepTac [variableClauseMachine, variableConfiguration, variablePayloadLabel, - variablePayloadStatement] + fin_cases position <;> + reduceMachineConfiguration + [variableConfiguration] + (compactMachineStepTac [ + variableClauseMachine, + variableConfiguration, + variablePayloadLabel, + variablePayloadStatement]) theorem variableSignStep (position : Fin 3) (hposition : position ≠ 2) @@ -648,12 +664,17 @@ theorem variableSignStep some (variableConfiguration (variablePrefixLabel (nextLiteralPosition position)) input [] count) := by - fin_cases position <;> cases sign <;> - first + fin_cases position <;> first | exact (hposition rfl).elim - | compactMachineStepTac [variableClauseMachine, variableConfiguration, - variablePrefixLabel, variablePayloadLabel, nextLiteralPosition, - variablePayloadStatement] + | reduceMachineConfiguration + [variableConfiguration] + (compactMachineStepTac [ + variableClauseMachine, + variableConfiguration, + variablePrefixLabel, + variablePayloadLabel, + nextLiteralPosition, + variablePayloadStatement]) theorem variableCompleteClauseStep (sign : Bool) (input : List Bool) (count : ℕ) : @@ -662,18 +683,28 @@ theorem variableCompleteClauseStep (sign :: input) [] count) = some (variableConfiguration (variablePrefixLabel 0) input [] (count + 1)) := by - cases sign <;> - compactMachineStepTac [variableClauseMachine, variableConfiguration, - variablePrefixLabel, variablePayloadLabel, variablePayloadStatement, - List.replicate_succ] + reduceMachineConfiguration + [variableConfiguration] + (compactMachineStepTac [ + variableClauseMachine, + variableConfiguration, + variablePrefixLabel, + variablePayloadLabel, + variablePayloadStatement, + List.replicate_succ]) theorem variableFinishValid (count : ℕ) : variableClauseMachine.step (variableConfiguration (variablePrefixLabel 0) [] [] count) = some (Turing.haltList variableClauseMachine (true :: List.replicate count true)) := by - compactMachineStepTac [variableClauseMachine, variableConfiguration, variablePrefixLabel, - variablePrefixStatement] + reduceMachineConfiguration + [variableConfiguration] + (compactMachineStepTac [ + variableClauseMachine, + variableConfiguration, + variablePrefixLabel, + variablePrefixStatement]) theorem variablePrefixUnfinished (position : Fin 3) (bit : Bool) @@ -682,9 +713,8 @@ theorem variablePrefixUnfinished (variableConfiguration (variablePrefixLabel position) [] (bit :: counter) count) = some (variableConfiguration 6 [] (bit :: counter) count) := by - fin_cases position <;> cases bit <;> - compactMachineStepTac [variableClauseMachine, variableConfiguration, variablePrefixLabel, - variablePrefixStatement] + fin_cases position <;> + rfl theorem variablePrefixIncompleteClause (position : Fin 3) (hposition : position ≠ 0) (count : ℕ) : @@ -705,29 +735,31 @@ theorem variablePayloadMissing [] counter count) = some (variableConfiguration 6 [] counter count) := by fin_cases position <;> cases counter <;> - compactMachineStepTac [variableClauseMachine, variableConfiguration, variablePayloadLabel, - variablePayloadStatement] + rfl theorem variableFailureDropInput (bit : Bool) (input counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration 6 (bit :: input) counter count) = some (variableConfiguration 6 input counter count) := by - cases bit <;> compactMachineStepTac [variableClauseMachine, variableConfiguration] + machineStackEquality [ + variableClauseMachine, variableConfiguration] theorem variableFailureDropCounter (bit : Bool) (counter : List Bool) (count : ℕ) : variableClauseMachine.step (variableConfiguration 6 [] (bit :: counter) count) = some (variableConfiguration 6 [] counter count) := by - cases bit <;> compactMachineStepTac [variableClauseMachine, variableConfiguration] + machineStackEquality [ + variableClauseMachine, variableConfiguration] theorem variableFailureFinish (count : ℕ) : variableClauseMachine.step (variableConfiguration 6 [] [] count) = some (Turing.haltList variableClauseMachine (false :: List.replicate count true)) := by - compactMachineStepTac [variableClauseMachine, variableConfiguration] + machineStackEquality [ + variableClauseMachine, variableConfiguration] /-- Clear the decoder work stacks and emit a failure marker. -/ def variableFailureTrace @@ -1058,7 +1090,7 @@ private theorem binaryStackValue_encodeNum (value : Num) : | zero => rfl | pos value => - simpa only [Computability.encodeNum, Num.cast_pos] using binaryStackValue_encodePosNum value + exact binaryStackValue_encodePosNum value /-- Internal support shared across GapCVP continuation modules. -/ theorem binaryStackValue_encodeNat (value : ℕ) : @@ -1111,8 +1143,7 @@ theorem binaryStackValue_eq_zero_iff | nil => simp only [binaryStackValue, List.not_mem_nil, IsEmpty.forall_iff, implies_true] | cons bit bits ih => - cases bit <;> - simp [binaryStackValue, ih] + simp [binaryStackValue, ih] /-- GapCVP reduction support. -/ def canonicalPrefixLabel (position : Fin 3) : Fin 17 := @@ -1300,7 +1331,8 @@ theorem canonical_header_prefix_true counter field binary borrow output) = some (canonicalConfiguration 0 input (true :: counter) field binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalHeaderPrefixDelimiter (input counter field binary borrow output : List Bool) : @@ -1309,7 +1341,8 @@ theorem canonicalHeaderPrefixDelimiter counter field binary borrow output) = some (canonicalConfiguration 1 input counter field binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_prefix_missing @@ -1319,7 +1352,7 @@ theorem canonical_header_prefix_missing counter field binary borrow output) = some (canonicalConfiguration 15 [] counter field binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_payload_step @@ -1329,7 +1362,8 @@ theorem canonical_header_payload_step (true :: counter) field binary borrow output) = some (canonicalConfiguration 1 input counter (bit :: field) binary borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_payload_missing @@ -1339,7 +1373,7 @@ theorem canonical_header_payload_missing field binary borrow output) = some (canonicalConfiguration 15 [] (true :: counter) field binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_payload_complete @@ -1349,7 +1383,7 @@ theorem canonical_header_payload_complete field binary borrow output) = some (canonicalConfiguration 2 input [] field binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_check_true @@ -1359,7 +1393,7 @@ theorem canonical_header_check_true (true :: field) binary borrow output) = some (canonicalConfiguration 3 input [] (true :: field) binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_check_false @@ -1369,7 +1403,7 @@ theorem canonical_header_check_false (false :: field) binary borrow output) = some (canonicalConfiguration 15 input [] (false :: field) binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_header_check_zero @@ -1379,7 +1413,7 @@ theorem canonical_header_check_zero [] binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel 0) input [] [] binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalPrefixLabel] + rfl theorem canonicalHeaderReverseStep (bit : Bool) (input field binary borrow output : List Bool) : @@ -1388,7 +1422,8 @@ theorem canonicalHeaderReverseStep (bit :: field) binary borrow output) = some (canonicalConfiguration 3 input [] field (bit :: binary) borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalHeaderReverseComplete (input binary borrow output : List Bool) : @@ -1397,7 +1432,7 @@ theorem canonicalHeaderReverseComplete [] binary borrow output) = some (canonicalConfiguration (canonicalPrefixLabel 0) input [] [] binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalPrefixLabel] + rfl theorem canonicalBorrowZero (input counter field binary borrow output : List Bool) : @@ -1406,7 +1441,8 @@ theorem canonicalBorrowZero (false :: binary) borrow output) = some (canonicalConfiguration 13 input counter field binary (true :: borrow) output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalBorrowOne (input counter field binary borrow output : List Bool) : @@ -1415,7 +1451,8 @@ theorem canonicalBorrowOne (true :: binary) borrow output) = some (canonicalConfiguration 14 input counter field (false :: binary) borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalBorrowExhausted (input counter field borrow output : List Bool) : @@ -1424,7 +1461,7 @@ theorem canonicalBorrowExhausted [] borrow output) = some (canonicalConfiguration 15 input counter field [] borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl theorem canonicalBorrowRestoreStep (bit : Bool) (input counter field binary borrow output : List Bool) : @@ -1433,7 +1470,8 @@ theorem canonicalBorrowRestoreStep binary (bit :: borrow) output) = some (canonicalConfiguration 14 input counter field (true :: binary) borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalBorrowRestoreComplete (input counter field binary output : List Bool) : @@ -1442,7 +1480,7 @@ theorem canonicalBorrowRestoreComplete binary [] output) = some (canonicalConfiguration (canonicalPrefixLabel 0) input counter field binary [] output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalPrefixLabel] + rfl theorem canonicalZeroCheckFalse (input counter field binary borrow output : List Bool) : @@ -1451,7 +1489,8 @@ theorem canonicalZeroCheckFalse (false :: binary) borrow output) = some (canonicalConfiguration 16 input counter field binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalZeroCheckTrue (input counter field binary borrow output : List Bool) : @@ -1460,13 +1499,17 @@ theorem canonicalZeroCheckTrue (true :: binary) borrow output) = some (canonicalConfiguration 15 input counter field (true :: binary) borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + rfl theorem canonicalZeroCheckFinish : canonicalFormulaMachine.step (canonicalConfiguration 16 [] [] [] [] [] []) = some (Turing.haltList canonicalFormulaMachine [true]) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_prefix_true @@ -1478,9 +1521,13 @@ theorem canonical_literal_prefix_true some (canonicalConfiguration (canonicalPrefixLabel position) input (true :: counter) field binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, + reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, canonicalPrefixLabel, - canonicalPrefixStatement] + canonicalPrefixStatement]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_prefix_delimiter @@ -1492,9 +1539,14 @@ theorem canonical_literal_prefix_delimiter some (canonicalConfiguration (canonicalPayloadLabel position) input counter field binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, + reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, canonicalPrefixLabel, - canonicalPayloadLabel, canonicalPrefixStatement] + canonicalPayloadLabel, + canonicalPrefixStatement]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_payload_step @@ -1506,9 +1558,13 @@ theorem canonical_literal_payload_step field binary borrow output) = some (canonicalConfiguration (canonicalPayloadLabel position) input counter (bit :: field) binary borrow output) := by - fin_cases position <;> cases bit <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalPayloadStatement] + fin_cases position <;> reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, + canonicalPayloadLabel, + canonicalPayloadStatement]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_payload_missing @@ -1520,8 +1576,7 @@ theorem canonical_literal_payload_missing some (canonicalConfiguration 15 [] (true :: counter) field binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalPayloadStatement] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_field_true @@ -1533,8 +1588,7 @@ theorem canonical_literal_field_true some (canonicalConfiguration (canonicalClearLabel position) input [] (true :: field) binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalClearLabel, canonicalPayloadStatement] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_field_false @@ -1546,8 +1600,7 @@ theorem canonical_literal_field_false some (canonicalConfiguration 15 input [] (false :: field) binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalPayloadStatement] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_clear_step @@ -1558,9 +1611,14 @@ theorem canonical_literal_clear_step input [] (bit :: field) binary borrow output) = some (canonicalConfiguration (canonicalClearLabel position) input [] field binary borrow output) := by - fin_cases position <;> cases bit <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalClearLabel, - canonicalClearStatement] + fin_cases position <;> + reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, + canonicalClearLabel, + canonicalClearStatement]) theorem canonicalClearSignStep (position : Fin 3) (hposition : position ≠ 2) @@ -1571,12 +1629,18 @@ theorem canonicalClearSignStep some (canonicalConfiguration (canonicalPrefixLabel (nextLiteralPosition position)) input [] [] binary borrow output) := by - fin_cases position <;> cases sign <;> - first + fin_cases position <;> first | exact (hposition rfl).elim - | compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalClearLabel, canonicalPrefixLabel, canonicalClearStatement, - canonicalSignStatement, nextLiteralPosition] + | reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, + canonicalClearLabel, + canonicalPrefixLabel, + canonicalClearStatement, + canonicalSignStatement, + nextLiteralPosition]) theorem canonicalClearCompleteClause (sign : Bool) (input binary borrow output : List Bool) : @@ -1585,9 +1649,14 @@ theorem canonicalClearCompleteClause (sign :: input) [] [] binary borrow output) = some (canonicalConfiguration 13 input [] [] binary borrow output) := by - cases sign <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalClearLabel, - canonicalClearStatement, canonicalSignStatement] + reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, + canonicalClearLabel, + canonicalClearStatement, + canonicalSignStatement]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_zero_field_sign_step @@ -1599,12 +1668,18 @@ theorem canonical_zero_field_sign_step some (canonicalConfiguration (canonicalPrefixLabel (nextLiteralPosition position)) input [] [] binary borrow output) := by - fin_cases position <;> cases sign <;> - first + fin_cases position <;> first | exact (hposition rfl).elim - | compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalPrefixLabel, canonicalPayloadStatement, - canonicalSignStatement, nextLiteralPosition] + | reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, + canonicalPayloadLabel, + canonicalPrefixLabel, + canonicalPayloadStatement, + canonicalSignStatement, + nextLiteralPosition]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_zero_field_completeClause @@ -1614,9 +1689,14 @@ theorem canonical_zero_field_completeClause (sign :: input) [] [] binary borrow output) = some (canonicalConfiguration 13 input [] [] binary borrow output) := by - cases sign <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalPayloadStatement, canonicalSignStatement] + reduceMachineConfiguration + [canonicalConfiguration] + (compactMachineStepTac [ + canonicalFormulaMachine, + canonicalConfiguration, + canonicalPayloadLabel, + canonicalPayloadStatement, + canonicalSignStatement]) /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_body_finish @@ -1626,8 +1706,7 @@ theorem canonical_body_finish [] [] [] binary borrow output) = some (canonicalConfiguration 16 [] [] [] binary borrow output) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalPrefixLabel, - canonicalPrefixStatement] + rfl /-- Borrow across zero bits until a one bit is reached. -/ def canonicalBorrowZerosTrace @@ -1725,7 +1804,8 @@ theorem canonicalFailureDropInput counter field binary borrow output) = some (canonicalConfiguration 15 input counter field binary borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalFailureDropCounter (bit : Bool) @@ -1735,7 +1815,8 @@ theorem canonicalFailureDropCounter (bit :: counter) field binary borrow output) = some (canonicalConfiguration 15 [] counter field binary borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalFailureDropField (bit : Bool) (field binary borrow output : List Bool) : @@ -1744,7 +1825,8 @@ theorem canonicalFailureDropField (bit :: field) binary borrow output) = some (canonicalConfiguration 15 [] [] field binary borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalFailureDropBinary (bit : Bool) (binary borrow output : List Bool) : @@ -1753,7 +1835,8 @@ theorem canonicalFailureDropBinary (bit :: binary) borrow output) = some (canonicalConfiguration 15 [] [] [] binary borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalFailureDropBorrow (bit : Bool) (borrow output : List Bool) : @@ -1762,14 +1845,16 @@ theorem canonicalFailureDropBorrow (bit :: borrow) output) = some (canonicalConfiguration 15 [] [] [] [] borrow output) := by - cases bit <;> compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] theorem canonicalFailureFinish (output : List Bool) : canonicalFormulaMachine.step (canonicalConfiguration 15 [] [] [] [] [] output) = some (Turing.haltList canonicalFormulaMachine (false :: output)) := by - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration] + machineStackEquality [ + canonicalFormulaMachine, canonicalConfiguration] /-- Internal support shared across GapCVP continuation modules. -/ def canonicalFailureTrace @@ -1916,7 +2001,7 @@ theorem encodeNat_canonical (number : ℕ) : | zero => simp only [isCanonicalBinaryWord, Computability.encodeNum, List.reverse_nil] | pos positive => - simpa only [Computability.encodeNum] using encodePosNum_canonical positive + exact encodePosNum_canonical positive /-- Internal support shared across GapCVP continuation modules. -/ def canonicalHeaderPrefixTrace @@ -2247,10 +2332,7 @@ theorem canonical_literal_prefix_missing_counter [] (counterBit :: counter) field binary borrow output) = some (canonicalConfiguration 15 [] (counterBit :: counter) field binary borrow output) := by - fin_cases position <;> cases counterBit <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPrefixLabel, - canonicalPrefixStatement] + fin_cases position <;> rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_literal_prefix_incomplete @@ -2276,8 +2358,7 @@ theorem canonical_zero_field_missing_sign some (canonicalConfiguration 15 [] [] [] binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, - canonicalPayloadLabel, canonicalPayloadStatement, canonicalSignStatement] + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem canonical_clear_missing_sign @@ -2288,8 +2369,7 @@ theorem canonical_clear_missing_sign some (canonicalConfiguration 15 [] [] [] binary borrow output) := by fin_cases position <;> - compactMachineStepTac [canonicalFormulaMachine, canonicalConfiguration, canonicalClearLabel, - canonicalClearStatement, canonicalSignStatement] + rfl end FormulaTotalCert diff --git a/LeanPool/GapCVP/Part03D.lean b/LeanPool/GapCVP/Part03D.lean index 532220e358..158d7701c5 100644 --- a/LeanPool/GapCVP/Part03D.lean +++ b/LeanPool/GapCVP/Part03D.lean @@ -1526,7 +1526,7 @@ private theorem structuralBinaryIncrement_encodeNat (number : ℕ) : | zero => rfl | pos positive => - simpa only [Computability.encodeNum, Num.succ, Num.succ'] using + exact structuralBinaryIncrement_encodePosNum positive /-- Split an increment into the number of cleared low digits and the remaining high digits. -/ @@ -1576,8 +1576,7 @@ private theorem structuralBinaryIncrement_length_le | false => simp only [structuralBinaryIncrement, List.length_cons, le_add_iff_nonneg_right, zero_le] | true => - simpa only [structuralBinaryIncrement, List.length_cons, Nat.add_assoc, Nat.reduceAdd, - add_le_add_iff_right] using Nat.add_le_add_right ih 1 + exact Nat.add_le_add_right ih 1 /-- Apply binary increment the specified number of times. -/ def structuralBinaryIncrementN : ℕ → List Bool → List Bool @@ -1765,6 +1764,16 @@ macro "naturalBinaryWriterStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a natural binary writer step using the fixed simplification rules. -/ +macro "naturalBinaryWriterStepOnly" : tactic => + `(tactic| machineStackEquality [ + structuralNaturalBinaryWriter, naturalBinaryWriterConfiguration, naturalBinaryWriterPeek, + naturalBinaryWriterPop, naturalBinaryWriterPushBit, naturalBinaryWriterPushConstant, + naturalBinaryWriterGoto, naturalBinaryWriterInputStatement, + naturalBinaryWriterCarryStatement, naturalBinaryWriterRestoreStatement, + naturalBinaryWriterPrepareStatement, naturalBinaryWriterOutputStatement, Turing.haltList, + Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + theorem naturalBinaryWriterInputStep (bit : Bool) (input digits carry output : List Bool) : structuralNaturalBinaryWriter.step @@ -1772,7 +1781,7 @@ theorem naturalBinaryWriterInputStep (bit : Bool) (bit :: input) digits carry output) = some (naturalBinaryWriterConfiguration 1 input digits carry output) := by - cases bit <;> naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterInputFinish (digits carry output : List Bool) : @@ -1780,7 +1789,7 @@ theorem naturalBinaryWriterInputFinish (naturalBinaryWriterConfiguration 0 [] digits carry output) = some (naturalBinaryWriterConfiguration 3 [] digits carry output) := by - naturalBinaryWriterStepTac + rfl theorem naturalBinaryWriterCarryTrueStep (input digits carry output : List Bool) : @@ -1789,7 +1798,7 @@ theorem naturalBinaryWriterCarryTrueStep input (true :: digits) carry output) = some (naturalBinaryWriterConfiguration 1 input digits (false :: carry) output) := by - naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterCarryFalseStep (input digits carry output : List Bool) : @@ -1798,7 +1807,7 @@ theorem naturalBinaryWriterCarryFalseStep input (false :: digits) carry output) = some (naturalBinaryWriterConfiguration 2 input (true :: digits) carry output) := by - naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterCarryEmptyStep (input carry output : List Bool) : @@ -1807,7 +1816,7 @@ theorem naturalBinaryWriterCarryEmptyStep input [] carry output) = some (naturalBinaryWriterConfiguration 2 input [true] carry output) := by - naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterRestoreStep (bit : Bool) (input digits carry output : List Bool) : @@ -1816,7 +1825,7 @@ theorem naturalBinaryWriterRestoreStep (bit : Bool) input digits (bit :: carry) output) = some (naturalBinaryWriterConfiguration 2 input (bit :: digits) carry output) := by - cases bit <;> naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterRestoreFinish (input digits output : List Bool) : @@ -1825,7 +1834,7 @@ theorem naturalBinaryWriterRestoreFinish input digits [] output) = some (naturalBinaryWriterConfiguration 0 input digits [] output) := by - naturalBinaryWriterStepTac + rfl theorem naturalBinaryWriterPrepareStep (bit : Bool) (digits carry output : List Bool) : @@ -1834,7 +1843,7 @@ theorem naturalBinaryWriterPrepareStep (bit : Bool) [] (bit :: digits) carry output) = some (naturalBinaryWriterConfiguration 3 [] digits (bit :: carry) output) := by - cases bit <;> naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterPrepareFinish (carry output : List Bool) : @@ -1842,7 +1851,7 @@ theorem naturalBinaryWriterPrepareFinish (naturalBinaryWriterConfiguration 3 [] [] carry output) = some (naturalBinaryWriterConfiguration 4 [] [] carry output) := by - naturalBinaryWriterStepTac + rfl theorem naturalBinaryWriterOutputStep (bit : Bool) (carry output : List Bool) : @@ -1851,13 +1860,13 @@ theorem naturalBinaryWriterOutputStep (bit : Bool) [] [] (bit :: carry) output) = some (naturalBinaryWriterConfiguration 4 [] [] carry (bit :: output)) := by - cases bit <;> naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly theorem naturalBinaryWriterOutputFinish (output : List Bool) : structuralNaturalBinaryWriter.step (naturalBinaryWriterConfiguration 4 [] [] [] output) = some (Turing.haltList structuralNaturalBinaryWriter output) := by - naturalBinaryWriterStepTac + naturalBinaryWriterStepOnly /-- Propagate a carry to the first zero bit or the end of the binary counter. -/ def naturalBinaryWriterCarrySearchTrace diff --git a/LeanPool/GapCVP/Part03E.lean b/LeanPool/GapCVP/Part03E.lean index 89398de957..a857335b77 100644 --- a/LeanPool/GapCVP/Part03E.lean +++ b/LeanPool/GapCVP/Part03E.lean @@ -340,6 +340,21 @@ macro "delimitedCompareStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a delimited compare step using the fixed simplification rules. -/ +macro "delimitedCompareStepOnly" : tactic => + `(tactic| machineStackEquality [ + delimitedPairComparisonMachine, delimitedCompareConfiguration, delimitedComparePeekFirst, + delimitedComparePeekSecond, delimitedComparePop, delimitedComparePushFirst, + delimitedComparePushConstant, delimitedCompareGoto, delimitedCompareSetOutcome, + delimitedCompareFirstPrefixStatement, delimitedCompareFirstPayloadStatement, + delimitedCompareSecondPrefixStatement, delimitedCompareSecondPayloadStatement, + delimitedCompareReverseFirstStatement, delimitedCompareReverseSecondStatement, + delimitedCompareWordsStatement, delimitedCompareCleanupStatement, + delimitedCompareTrailingStatement, delimitedCompareOutcomeStatement, + delimitedCompareSourceStatement, delimitedComparePrefixStatement, encodedWordOrderingWord, + encodedWordOrderingFirst, encodedWordOrderingSecond, Turing.haltList, Turing.FinTM2.step, + Turing.TM2.step, Turing.TM2.stepAux]) + theorem delimitedCompare_firstPrefix_true (outcome : EncodedWordOrdering) (input firstCounter firstReversed secondCounter secondReversed @@ -353,7 +368,7 @@ theorem delimitedCompare_firstPrefix_true input (true :: firstCounter) firstReversed secondCounter secondReversed firstForward secondForward (true :: source) (true :: sourcePrefix) output) := by - delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_firstPrefix_delimiter (outcome : EncodedWordOrdering) @@ -368,7 +383,7 @@ theorem delimitedCompare_firstPrefix_delimiter input firstCounter firstReversed secondCounter secondReversed firstForward secondForward (false :: source) (true :: sourcePrefix) output) := by - delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_firstPrefix_missing (outcome : EncodedWordOrdering) @@ -383,7 +398,7 @@ theorem delimitedCompare_firstPrefix_missing [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_firstPayload_step (outcome : EncodedWordOrdering) (bit marker : Bool) @@ -398,7 +413,7 @@ theorem delimitedCompare_firstPayload_step input firstCounter (bit :: firstReversed) secondCounter secondReversed firstForward secondForward (bit :: source) (true :: sourcePrefix) output) := by - cases bit <;> cases marker <;> delimitedCompareStepTac + cases marker <;> delimitedCompareStepOnly theorem delimitedCompare_firstPayload_finish (outcome : EncodedWordOrdering) @@ -413,7 +428,7 @@ theorem delimitedCompare_firstPayload_finish input [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_firstPayload_missing (outcome : EncodedWordOrdering) (marker : Bool) @@ -428,7 +443,7 @@ theorem delimitedCompare_firstPayload_missing [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases marker <;> delimitedCompareStepTac + cases marker <;> delimitedCompareStepOnly theorem delimitedCompare_secondPrefix_true (outcome : EncodedWordOrdering) @@ -444,7 +459,7 @@ theorem delimitedCompare_secondPrefix_true (true :: secondCounter) secondReversed firstForward secondForward (true :: source) (true :: sourcePrefix) output) := by - delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_secondPrefix_delimiter (outcome : EncodedWordOrdering) @@ -459,7 +474,7 @@ theorem delimitedCompare_secondPrefix_delimiter input firstCounter firstReversed secondCounter secondReversed firstForward secondForward (false :: source) (true :: sourcePrefix) output) := by - delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_secondPrefix_missing (outcome : EncodedWordOrdering) @@ -474,7 +489,7 @@ theorem delimitedCompare_secondPrefix_missing [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_secondPayload_step (outcome : EncodedWordOrdering) (bit marker : Bool) @@ -490,7 +505,7 @@ theorem delimitedCompare_secondPayload_step secondCounter (bit :: secondReversed) firstForward secondForward (bit :: source) (true :: sourcePrefix) output) := by - cases bit <;> cases marker <;> delimitedCompareStepTac + cases marker <;> delimitedCompareStepOnly theorem delimitedCompare_secondPayload_finish (outcome : EncodedWordOrdering) @@ -505,7 +520,7 @@ theorem delimitedCompare_secondPayload_finish input firstCounter firstReversed [] secondReversed firstForward secondForward source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_secondPayload_missing (outcome : EncodedWordOrdering) (marker : Bool) @@ -520,7 +535,7 @@ theorem delimitedCompare_secondPayload_missing [] firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases marker <;> delimitedCompareStepTac + cases marker <;> delimitedCompareStepOnly theorem delimitedCompare_reverseFirst_step (outcome : EncodedWordOrdering) (bit : Bool) @@ -535,7 +550,7 @@ theorem delimitedCompare_reverseFirst_step input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_reverseFirst_finish (outcome : EncodedWordOrdering) @@ -550,7 +565,7 @@ theorem delimitedCompare_reverseFirst_finish input firstCounter [] secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_reverseSecond_step (outcome : EncodedWordOrdering) (bit : Bool) @@ -565,7 +580,7 @@ theorem delimitedCompare_reverseSecond_step input firstCounter firstReversed secondCounter secondReversed firstForward (bit :: secondForward) source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_reverseSecond_finish (outcome : EncodedWordOrdering) @@ -580,7 +595,7 @@ theorem delimitedCompare_reverseSecond_finish input firstCounter firstReversed secondCounter [] firstForward secondForward source sourcePrefix output) := by - delimitedCompareStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem delimitedCompare_words_equalBit @@ -597,7 +612,7 @@ theorem delimitedCompare_words_equalBit input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + reduceMachineConfiguration [delimitedCompareConfiguration] (delimitedCompareStepTac) /-- Internal support shared across GapCVP continuation modules. -/ theorem delimitedCompare_words_lessBit @@ -615,7 +630,7 @@ theorem delimitedCompare_words_lessBit secondCounter secondReversed (false :: firstForward) (true :: secondForward) source sourcePrefix output) := by - delimitedCompareStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem delimitedCompare_words_greaterBit @@ -633,7 +648,7 @@ theorem delimitedCompare_words_greaterBit secondCounter secondReversed (true :: firstForward) (false :: secondForward) source sourcePrefix output) := by - delimitedCompareStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem delimitedCompare_words_firstEmpty @@ -649,7 +664,7 @@ theorem delimitedCompare_words_firstEmpty input firstCounter firstReversed secondCounter secondReversed [] (bit :: secondForward) source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem delimitedCompare_words_secondEmpty @@ -665,7 +680,7 @@ theorem delimitedCompare_words_secondEmpty input firstCounter firstReversed secondCounter secondReversed (bit :: firstForward) [] source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem delimitedCompare_words_bothEmpty @@ -681,7 +696,7 @@ theorem delimitedCompare_words_bothEmpty input firstCounter firstReversed secondCounter secondReversed [] [] source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_cleanup_firstCounter (outcome : EncodedWordOrdering) (bit : Bool) @@ -696,7 +711,7 @@ theorem delimitedCompare_cleanup_firstCounter input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_cleanup_firstReversed (outcome : EncodedWordOrdering) (bit : Bool) @@ -711,7 +726,7 @@ theorem delimitedCompare_cleanup_firstReversed input [] firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_cleanup_secondCounter (outcome : EncodedWordOrdering) (bit : Bool) @@ -724,7 +739,7 @@ theorem delimitedCompare_cleanup_secondCounter some (delimitedCompareConfiguration 7 outcome input [] [] secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_cleanup_secondReversed (outcome : EncodedWordOrdering) (bit : Bool) @@ -737,7 +752,7 @@ theorem delimitedCompare_cleanup_secondReversed some (delimitedCompareConfiguration 7 outcome input [] [] [] secondReversed firstForward secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_cleanup_firstForward (outcome : EncodedWordOrdering) (bit : Bool) @@ -750,7 +765,7 @@ theorem delimitedCompare_cleanup_firstForward some (delimitedCompareConfiguration 7 outcome input [] [] [] [] firstForward secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_cleanup_secondForward (outcome : EncodedWordOrdering) (bit : Bool) @@ -762,7 +777,7 @@ theorem delimitedCompare_cleanup_secondForward some (delimitedCompareConfiguration 7 outcome input [] [] [] [] [] secondForward source sourcePrefix output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_cleanup_finish (outcome : EncodedWordOrdering) @@ -772,7 +787,7 @@ theorem delimitedCompare_cleanup_finish input [] [] [] [] [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 8 outcome input [] [] [] [] [] [] source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_trailing_step (outcome : EncodedWordOrdering) (bit : Bool) @@ -783,7 +798,7 @@ theorem delimitedCompare_trailing_step some (delimitedCompareConfiguration 8 outcome input [] [] [] [] [] [] (bit :: source) (true :: sourcePrefix) output) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_trailing_finish (outcome : EncodedWordOrdering) @@ -793,7 +808,7 @@ theorem delimitedCompare_trailing_finish [] [] [] [] [] [] [] source sourcePrefix output) = some (delimitedCompareConfiguration 9 outcome [] [] [] [] [] [] [] source sourcePrefix output) := by - delimitedCompareStepTac + rfl theorem delimitedCompare_outcome_step (outcome : EncodedWordOrdering) @@ -804,7 +819,7 @@ theorem delimitedCompare_outcome_step some (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] source sourcePrefix (encodedWordOrderingWord outcome ++ output)) := by - cases outcome <;> delimitedCompareStepTac + cases outcome <;> delimitedCompareStepOnly theorem delimitedCompare_source_step (outcome : EncodedWordOrdering) (bit : Bool) @@ -814,7 +829,7 @@ theorem delimitedCompare_source_step [] [] [] [] [] [] [] (bit :: source) sourcePrefix output) = some (delimitedCompareConfiguration 10 outcome [] [] [] [] [] [] [] source sourcePrefix (bit :: output)) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_source_finish (outcome : EncodedWordOrdering) @@ -824,7 +839,7 @@ theorem delimitedCompare_source_finish [] [] [] [] [] [] [] [] sourcePrefix output) = some (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] sourcePrefix (false :: output)) := by - delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_prefix_step (outcome : EncodedWordOrdering) (bit : Bool) @@ -834,7 +849,7 @@ theorem delimitedCompare_prefix_step [] [] [] [] [] [] [] [] (bit :: sourcePrefix) output) = some (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] sourcePrefix (true :: output)) := by - cases bit <;> delimitedCompareStepTac + delimitedCompareStepOnly theorem delimitedCompare_prefix_finish (outcome : EncodedWordOrdering) (output : List Bool) : @@ -842,7 +857,7 @@ theorem delimitedCompare_prefix_finish (delimitedCompareConfiguration 11 outcome [] [] [] [] [] [] [] [] [] output) = some (Turing.haltList delimitedPairComparisonMachine output) := by - cases outcome <;> delimitedCompareStepTac + cases outcome <;> delimitedCompareStepOnly end CNFEncodedClauseSort diff --git a/LeanPool/GapCVP/Part03F.lean b/LeanPool/GapCVP/Part03F.lean index 11d759a236..77126dd8d6 100644 --- a/LeanPool/GapCVP/Part03F.lean +++ b/LeanPool/GapCVP/Part03F.lean @@ -1019,13 +1019,11 @@ theorem lexicographicEncodedWordResidualsFirstLengthLe | nil => simp only [lexicographicEncodedWordResiduals, List.length_cons, Std.le_refl] | cons next second => cases bit <;> cases next - · simpa only [lexicographicEncodedWordResiduals, List.length_cons, Nat.succ_eq_add_one] - using + · exact Nat.le_trans (ih second) (Nat.le_succ remaining.length) · simp only [lexicographicEncodedWordResiduals, List.length_cons, Std.le_refl] · simp only [lexicographicEncodedWordResiduals, List.length_cons, Std.le_refl] - · simpa only [lexicographicEncodedWordResiduals, List.length_cons, Nat.succ_eq_add_one] - using + · exact Nat.le_trans (ih second) (Nat.le_succ remaining.length) theorem lexicographicEncodedWordResidualsSecondLengthLe @@ -1039,13 +1037,11 @@ theorem lexicographicEncodedWordResidualsSecondLengthLe | nil => simp only [lexicographicEncodedWordResiduals, List.length_nil, Std.le_refl] | cons next second => cases bit <;> cases next - · simpa only [lexicographicEncodedWordResiduals, List.length_cons, Nat.succ_eq_add_one] - using + · exact Nat.le_trans (ih second) (Nat.le_succ second.length) · simp only [lexicographicEncodedWordResiduals, List.length_cons, Std.le_refl] · simp only [lexicographicEncodedWordResiduals, List.length_cons, Std.le_refl] - · simpa only [lexicographicEncodedWordResiduals, List.length_cons, Nat.succ_eq_add_one] - using + · exact Nat.le_trans (ih second) (Nat.le_succ second.length) /-- Parses both records, runs a supplied phase-six comparison, and restores the input. -/ diff --git a/LeanPool/GapCVP/Part04A.lean b/LeanPool/GapCVP/Part04A.lean index 43feebb1c2..d75e0972c5 100644 --- a/LeanPool/GapCVP/Part04A.lean +++ b/LeanPool/GapCVP/Part04A.lean @@ -354,7 +354,7 @@ theorem naturalCompareWordsEqualBit some (naturalCompareConfiguration 6 outcome input firstCounter firstReversed secondCounter secondReversed firstForward secondForward source sourcePrefix output) := by - cases bit <;> naturalCompareStepTac + naturalCompareStepTac theorem naturalCompareWordsLessBit (outcome : EncodedWordOrdering) diff --git a/LeanPool/GapCVP/Part04B.lean b/LeanPool/GapCVP/Part04B.lean index 1e9103f74f..a6032cb90a 100644 --- a/LeanPool/GapCVP/Part04B.lean +++ b/LeanPool/GapCVP/Part04B.lean @@ -749,7 +749,7 @@ theorem polynomialRowMarkerHorner_eval have hdegree : polynomial.natDegree < polynomial.natDegree + 1 := by omega - simpa only using (Polynomial.eval_eq_sum_range' (x := value) hdegree).symm + exact (Polynomial.eval_eq_sum_range' (x := value) hdegree).symm /-- Internal support shared across GapCVP continuation modules. -/ abbrev PolynomialRowMarkerStage (polynomial : Polynomial ℕ) := @@ -1115,6 +1115,19 @@ macro "polynomialRowMarkerStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a polynomial row marker step using the fixed simplification rules. -/ +macro "polynomialRowMarkerStepOnly" : tactic => + `(tactic| machineStackEquality [ + polynomialRowMarkerMachine, polynomialRowMarkerConfiguration, polynomialRowMarkerPeek, + polynomialRowMarkerPop, polynomialRowMarkerPushBit, polynomialRowMarkerPushConstant, + polynomialRowMarkerGoto, polynomialRowMarkerScanStatement, + polynomialRowMarkerMultiplyStatement, polynomialRowMarkerBaseStatement, + polynomialRowMarkerRestoreBaseStatement, polynomialRowMarkerCoefficientStatement, + polynomialRowMarkerPayloadStatement, polynomialRowMarkerHeaderStatement, + polynomialRowMarkerSourceStatement, polynomialRowMarkerPrefixStatement, + polynomialRowMarkerPushBits_stepAux, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_scan_step (polynomial : Polynomial ℕ) @@ -1130,7 +1143,7 @@ theorem polynomialRowMarker_scan_step (polynomialRowMarkerConfiguration polynomial 0 stage input (bit :: source) (true :: base) baseScratch accumulator product output) := by - cases bit <;> polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_scan_finish @@ -1144,7 +1157,7 @@ theorem polynomialRowMarker_scan_finish some (polynomialRowMarkerConfiguration polynomial 1 stage [] source base baseScratch accumulator product output) := by - polynomialRowMarkerStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_multiply_step @@ -1159,7 +1172,7 @@ theorem polynomialRowMarker_multiply_step some (polynomialRowMarkerConfiguration polynomial 2 stage [] source base baseScratch accumulator product output) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_multiply_finish @@ -1172,7 +1185,7 @@ theorem polynomialRowMarker_multiply_finish some (polynomialRowMarkerConfiguration polynomial 4 stage [] source base baseScratch [] product output) := by - polynomialRowMarkerStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_base_step @@ -1188,7 +1201,7 @@ theorem polynomialRowMarker_base_step (polynomialRowMarkerConfiguration polynomial 2 stage [] source base (true :: baseScratch) accumulator (true :: product) output) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_base_finish @@ -1201,7 +1214,7 @@ theorem polynomialRowMarker_base_finish some (polynomialRowMarkerConfiguration polynomial 3 stage [] source [] baseScratch accumulator product output) := by - polynomialRowMarkerStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_restoreBase_step @@ -1217,7 +1230,7 @@ theorem polynomialRowMarker_restoreBase_step (polynomialRowMarkerConfiguration polynomial 3 stage [] source (true :: base) baseScratch accumulator product output) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_restoreBase_finish @@ -1230,7 +1243,7 @@ theorem polynomialRowMarker_restoreBase_finish some (polynomialRowMarkerConfiguration polynomial 1 stage [] source base [] accumulator product output) := by - polynomialRowMarkerStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_product_step @@ -1243,7 +1256,7 @@ theorem polynomialRowMarker_product_step some (polynomialRowMarkerConfiguration polynomial 4 stage [] source base [] (true :: accumulator) product output) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_coefficient_zero_step @@ -1262,7 +1275,7 @@ theorem polynomialRowMarker_coefficient_zero_step [] output) := by have hstage' : stage = (0 : PolynomialRowMarkerStage polynomial) := Fin.ext hstage - polynomialRowMarkerStepTac; + polynomialRowMarkerStepOnly; simp only [Fin.isValue, hstage', ↓reduceDIte, Fin.coe_ofNat_eq_mod, Nat.zero_mod, polynomialRowMarkerPushBits_stepAux, TM2.stepAux, List.reverse_replicate, Matrix.cons_val]; try { congr 2; funext stack; fin_cases stack <;> @@ -1307,7 +1320,7 @@ theorem polynomialRowMarker_payload_step (polynomialRowMarkerConfiguration polynomial 5 stage [] source base [] accumulator (true :: product) (true :: output)) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_payload_finish @@ -1320,7 +1333,7 @@ theorem polynomialRowMarker_payload_finish some (polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] product (false :: output)) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_header_step @@ -1333,7 +1346,7 @@ theorem polynomialRowMarker_header_step some (polynomialRowMarkerConfiguration polynomial 6 stage [] source base [] [] product (true :: output)) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_header_finish @@ -1346,7 +1359,7 @@ theorem polynomialRowMarker_header_finish some (polynomialRowMarkerConfiguration polynomial 7 stage [] source base [] [] [] output) := by - polynomialRowMarkerStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_source_step @@ -1360,7 +1373,7 @@ theorem polynomialRowMarker_source_step some (polynomialRowMarkerConfiguration polynomial 7 stage [] source base [] [] [] (bit :: output)) := by - cases bit <;> polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_source_finish @@ -1373,7 +1386,7 @@ theorem polynomialRowMarker_source_finish some (polynomialRowMarkerConfiguration polynomial 8 stage [] [] base [] [] [] (false :: output)) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_prefix_step @@ -1386,7 +1399,7 @@ theorem polynomialRowMarker_prefix_step some (polynomialRowMarkerConfiguration polynomial 8 stage [] [] base [] [] [] (true :: output)) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem polynomialRowMarker_finish @@ -1399,7 +1412,7 @@ theorem polynomialRowMarker_finish some (Turing.haltList (polynomialRowMarkerMachine polynomial) output) := by - polynomialRowMarkerStepTac + polynomialRowMarkerStepOnly end CNFPolynomialRowMarkerTM diff --git a/LeanPool/GapCVP/Part04D.lean b/LeanPool/GapCVP/Part04D.lean index 8b57b6f205..2011599f49 100644 --- a/LeanPool/GapCVP/Part04D.lean +++ b/LeanPool/GapCVP/Part04D.lean @@ -1063,8 +1063,7 @@ theorem boundedFold_restore_step (computer.inputAlphabet.invFun bit :: input) counter scratch) := by classical - cases bit <;> - compactMachineStepTac [boundedDependentRecordFoldMachine, + compactMachineStepTac [boundedDependentRecordFoldMachine, boundedFoldRestoreConfiguration, boundedFoldPhaseConfiguration, boundedFoldStacks, Turing.initList] all_goals diff --git a/LeanPool/GapCVP/Part04E.lean b/LeanPool/GapCVP/Part04E.lean index 0838889819..1282037acf 100644 --- a/LeanPool/GapCVP/Part04E.lean +++ b/LeanPool/GapCVP/Part04E.lean @@ -424,7 +424,7 @@ private theorem boundedFoldRunBudget_le | zero => simp only [boundedFoldRunBudget, zero_mul, zero_add, Std.le_refl] | succ count ih => have hseed : seed.length ≤ bound.eval inputLength := by - simpa only [Function.iterate_zero, id_eq] using hstates 0 (by omega) + exact hstates 0 (by omega) have htime : computer.time.eval seed.length ≤ computer.time.eval (bound.eval inputLength) := @@ -432,13 +432,13 @@ private theorem boundedFoldRunBudget_le computer.time hseed have houtput : (worker seed).length ≤ bound.eval inputLength := by - simpa only [Function.iterate_one] using hstates 1 (by omega) + exact hstates 1 (by omega) have hremaining : ∀ stage : ℕ, stage ≤ count → ((worker^[stage]) (worker seed)).length ≤ bound.eval inputLength := by intro stage hstage - simpa only [Function.iterate_succ_apply] using + exact hstates (stage + 1) (by omega) have htail := ih (worker seed) hremaining let cost := @@ -447,7 +447,7 @@ private theorem boundedFoldRunBudget_le have htail' : boundedFoldRunBudget computer count (worker seed) ≤ count * cost + 1 := by - simpa only using htail + exact htail change 1 + computer.time.eval seed.length + (2 * (worker seed).length + 2) + @@ -866,6 +866,17 @@ macro "flatLiteralRecordStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a flat literal record step using the fixed simplification rules. -/ +macro "flatLiteralRecordStepOnly" : tactic => + `(tactic| machineStackEquality [ + actualFlatLiteralRecordWorker, flatLiteralRecordConfiguration, flatLiteralRecordPeek, + flatLiteralRecordPop, flatLiteralRecordPushBit, flatLiteralRecordPushConstant, + flatLiteralRecordGoto, flatLiteralRecordPrefixStatement, flatLiteralRecordSignStatement, + flatLiteralRecordPayloadStatement, flatLiteralRecordRestoreStatement, + flatLiteralRecordMarkerStatement, flatLiteralRecordSuffixScanStatement, + flatLiteralRecordSuffixRestoreStatement, flatLiteralRecordInvalidStatement, + Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_prefix_true (sign : Option Bool) @@ -875,7 +886,7 @@ theorem flatLiteralRecord_prefix_true (true :: input) count reversed markers suffix output) = some (flatLiteralRecordConfiguration 0 sign input (true :: count) reversed markers suffix output) := by - flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_prefix_false @@ -886,7 +897,7 @@ theorem flatLiteralRecord_prefix_false (false :: input) count reversed markers suffix output) = some (flatLiteralRecordConfiguration 1 sign input count reversed markers suffix output) := by - flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_prefix_missing @@ -897,7 +908,7 @@ theorem flatLiteralRecord_prefix_missing [] count reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] count reversed markers suffix output) := by - flatLiteralRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_sign_step @@ -909,7 +920,7 @@ theorem flatLiteralRecord_sign_step reversed markers suffix output) = some (flatLiteralRecordConfiguration 2 (some sign) input count reversed markers suffix output) := by - cases sign <;> cases marker <;> flatLiteralRecordStepTac + cases marker <;> flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_sign_empty @@ -920,7 +931,7 @@ theorem flatLiteralRecord_sign_empty input [] reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign input [] reversed markers suffix output) := by - flatLiteralRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_sign_missing @@ -931,7 +942,7 @@ theorem flatLiteralRecord_sign_missing [] (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] (marker :: count) reversed markers suffix output) := by - cases marker <;> flatLiteralRecordStepTac + cases marker <;> rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_payload_step @@ -943,7 +954,7 @@ theorem flatLiteralRecord_payload_step reversed markers suffix output) = some (flatLiteralRecordConfiguration 2 sign input count (bit :: reversed) (true :: markers) suffix output) := by - cases bit <;> cases marker <;> flatLiteralRecordStepTac + cases marker <;> flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_payload_finish @@ -954,7 +965,7 @@ theorem flatLiteralRecord_payload_finish input [] reversed markers suffix output) = some (flatLiteralRecordConfiguration 3 (some sign) input [] reversed markers suffix (sign :: output)) := by - cases sign <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_payload_missing @@ -965,7 +976,7 @@ theorem flatLiteralRecord_payload_missing [] (marker :: count) reversed markers suffix output) = some (flatLiteralRecordConfiguration 7 sign [] (marker :: count) reversed markers suffix output) := by - cases marker <;> flatLiteralRecordStepTac + cases marker <;> rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_restore_step @@ -976,7 +987,7 @@ theorem flatLiteralRecord_restore_step input [] (bit :: reversed) markers suffix output) = some (flatLiteralRecordConfiguration 3 sign input [] reversed markers suffix (bit :: output)) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_restore_finish @@ -987,7 +998,7 @@ theorem flatLiteralRecord_restore_finish input [] [] markers suffix output) = some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (false :: output)) := by - flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_marker_step @@ -998,7 +1009,7 @@ theorem flatLiteralRecord_marker_step input [] [] (marker :: markers) suffix output) = some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (true :: output)) := by - cases marker <;> flatLiteralRecordStepTac + cases marker <;> flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_marker_finish @@ -1009,7 +1020,7 @@ theorem flatLiteralRecord_marker_finish input [] [] [] suffix output) = some (flatLiteralRecordConfiguration 5 sign input [] [] [] suffix output) := by - flatLiteralRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_suffix_scan_step @@ -1020,7 +1031,7 @@ theorem flatLiteralRecord_suffix_scan_step (bit :: input) [] [] [] suffix output) = some (flatLiteralRecordConfiguration 5 sign input [] [] [] (bit :: suffix) output) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_suffix_scan_finish @@ -1030,7 +1041,7 @@ theorem flatLiteralRecord_suffix_scan_finish [] [] [] [] suffix output) = some (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix output) := by - flatLiteralRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_suffix_restore_step @@ -1041,7 +1052,7 @@ theorem flatLiteralRecord_suffix_restore_step [] [] [] [] (bit :: suffix) output) = some (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix (bit :: output)) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_suffix_restore_finish @@ -1050,7 +1061,7 @@ theorem flatLiteralRecord_suffix_restore_finish (flatLiteralRecordConfiguration 6 sign [] [] [] [] [] output) = some (Turing.haltList actualFlatLiteralRecordWorker output) := by - flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_invalid_count @@ -1061,7 +1072,7 @@ theorem flatLiteralRecord_invalid_count input (bit :: count) reversed markers [] []) = some (flatLiteralRecordConfiguration 7 sign input count reversed markers [] []) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_invalid_reversed @@ -1072,7 +1083,7 @@ theorem flatLiteralRecord_invalid_reversed input [] (bit :: reversed) markers [] []) = some (flatLiteralRecordConfiguration 7 sign input [] reversed markers [] []) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_invalid_markers @@ -1083,7 +1094,7 @@ theorem flatLiteralRecord_invalid_markers input [] [] (bit :: markers) [] []) = some (flatLiteralRecordConfiguration 7 sign input [] [] markers [] []) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_invalid_input @@ -1093,7 +1104,7 @@ theorem flatLiteralRecord_invalid_input (bit :: input) [] [] [] [] []) = some (flatLiteralRecordConfiguration 7 sign input [] [] [] [] []) := by - cases bit <;> flatLiteralRecordStepTac + flatLiteralRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatLiteralRecord_invalid_finish (sign : Option Bool) : @@ -1101,7 +1112,7 @@ theorem flatLiteralRecord_invalid_finish (sign : Option Bool) : (flatLiteralRecordConfiguration 7 sign [] [] [] [] [] []) = some (Turing.haltList actualFlatLiteralRecordWorker []) := by - flatLiteralRecordStepTac + flatLiteralRecordStepOnly end CNFFlatStructuralRecordWorkerTM diff --git a/LeanPool/GapCVP/Part04F.lean b/LeanPool/GapCVP/Part04F.lean index 284c97403a..e73558ca9d 100644 --- a/LeanPool/GapCVP/Part04F.lean +++ b/LeanPool/GapCVP/Part04F.lean @@ -1389,6 +1389,17 @@ macro "unaryPairStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a unary pair step using the fixed simplification rules. -/ +macro "unaryPairStepOnly" : tactic => + `(tactic| machineStackEquality [ + actualUnaryPairIndexMachine, unaryPairConfiguration, unaryPairPeek, unaryPairPop, + unaryPairPush, unaryPairGoto, unaryPairFirstStatement, unaryPairSecondStatement, + unaryPairCompareStatement, unaryPairGreaterBaseStatement, unaryPairGreaterOffsetStatement, + unaryPairLessBaseStatement, unaryPairLessOffsetStatement, unaryPairOuterStatement, + unaryPairSquareCopyStatement, unaryPairSquareRestoreStatement, + unaryPairSquareCleanupStatement, unaryPairFailureStatement, Turing.haltList, + Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + theorem unaryPair_first_true (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : @@ -1399,7 +1410,7 @@ theorem unaryPair_first_true some (unaryPairConfiguration 0 input (true :: first) second matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_first_false @@ -1412,7 +1423,7 @@ theorem unaryPair_first_false some (unaryPairConfiguration 1 input first second matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + unaryPairStepOnly theorem unaryPair_first_missing (first second matchedFirst matchedSecond @@ -1424,7 +1435,7 @@ theorem unaryPair_first_missing some (unaryPairConfiguration 11 [] first second matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + rfl theorem unaryPair_second_true (input first second matchedFirst matchedSecond @@ -1436,7 +1447,7 @@ theorem unaryPair_second_true some (unaryPairConfiguration 1 input first (true :: second) matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_second_false @@ -1448,7 +1459,7 @@ theorem unaryPair_second_false base outer output scratch) = some (unaryPairConfiguration 2 input first second matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + unaryPairStepOnly theorem unaryPair_second_missing (first second matchedFirst matchedSecond @@ -1458,7 +1469,7 @@ theorem unaryPair_second_missing matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 11 [] first second matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_compare_match @@ -1471,7 +1482,7 @@ theorem unaryPair_compare_match some (unaryPairConfiguration 2 [] first second (true :: matchedFirst) (true :: matchedSecond) base outer output scratch) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_compare_greater @@ -1482,7 +1493,7 @@ theorem unaryPair_compare_greater matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 3 [] first [] matchedFirst matchedSecond base outer output scratch) := by - cases first <;> unaryPairStepTac + cases first <;> rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_compare_less @@ -1493,7 +1504,7 @@ theorem unaryPair_compare_less matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 5 [] [] (true :: second) matchedFirst matchedSecond base outer output scratch) := by - unaryPairStepTac + rfl theorem unaryPair_compare_trailing (bit : Bool) @@ -1506,7 +1517,7 @@ theorem unaryPair_compare_trailing some (unaryPairConfiguration 11 (bit :: input) first second matchedFirst matchedSecond base outer output scratch) := by - cases bit <;> unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_greater_base_first @@ -1518,7 +1529,7 @@ theorem unaryPair_greater_base_first some (unaryPairConfiguration 3 [] first [] matchedFirst matchedSecond (true :: base) (true :: outer) (true :: output) []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_greater_base_matched @@ -1530,7 +1541,7 @@ theorem unaryPair_greater_base_matched some (unaryPairConfiguration 3 [] [] [] matchedFirst matchedSecond (true :: base) (true :: outer) (true :: output) []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_greater_base_finish @@ -1540,7 +1551,7 @@ theorem unaryPair_greater_base_finish base outer output []) = some (unaryPairConfiguration 4 [] [] [] [] matchedSecond base outer output []) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_greater_offset_step @@ -1550,7 +1561,7 @@ theorem unaryPair_greater_offset_step (true :: matchedSecond) base outer output []) = some (unaryPairConfiguration 4 [] [] [] [] matchedSecond base outer (true :: output) []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_greater_offset_finish @@ -1560,7 +1571,7 @@ theorem unaryPair_greater_offset_finish base outer output []) = some (unaryPairConfiguration 7 [] [] [] [] [] base outer output []) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_less_base_second @@ -1571,7 +1582,7 @@ theorem unaryPair_less_base_second some (unaryPairConfiguration 5 [] [] second matchedFirst matchedSecond (true :: base) (true :: outer) output []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_less_base_matched @@ -1583,7 +1594,7 @@ theorem unaryPair_less_base_matched some (unaryPairConfiguration 5 [] [] [] matchedFirst matchedSecond (true :: base) (true :: outer) output []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_less_base_finish @@ -1593,7 +1604,7 @@ theorem unaryPair_less_base_finish base outer output []) = some (unaryPairConfiguration 6 [] [] [] matchedFirst [] base outer output []) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_less_offset_step @@ -1603,7 +1614,7 @@ theorem unaryPair_less_offset_step (true :: matchedFirst) [] base outer output []) = some (unaryPairConfiguration 6 [] [] [] matchedFirst [] base outer (true :: output) []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_less_offset_finish @@ -1613,7 +1624,7 @@ theorem unaryPair_less_offset_finish base outer output []) = some (unaryPairConfiguration 7 [] [] [] [] [] base outer output []) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_outer_step @@ -1623,7 +1634,7 @@ theorem unaryPair_outer_step base (true :: outer) output []) = some (unaryPairConfiguration 8 [] [] [] [] [] base outer output []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_outer_finish @@ -1633,7 +1644,7 @@ theorem unaryPair_outer_finish base [] output []) = some (unaryPairConfiguration 10 [] [] [] [] [] base [] output []) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_square_copy_step @@ -1643,7 +1654,7 @@ theorem unaryPair_square_copy_step (true :: base) outer output scratch) = some (unaryPairConfiguration 8 [] [] [] [] [] base outer (true :: output) (true :: scratch)) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_square_copy_finish @@ -1653,7 +1664,7 @@ theorem unaryPair_square_copy_finish [] outer output scratch) = some (unaryPairConfiguration 9 [] [] [] [] [] [] outer output scratch) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_square_restore_step @@ -1663,7 +1674,7 @@ theorem unaryPair_square_restore_step base outer output (true :: scratch)) = some (unaryPairConfiguration 9 [] [] [] [] [] (true :: base) outer output scratch) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_square_restore_finish @@ -1673,7 +1684,7 @@ theorem unaryPair_square_restore_finish base outer output []) = some (unaryPairConfiguration 7 [] [] [] [] [] base outer output []) := by - unaryPairStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_square_cleanup_step @@ -1683,14 +1694,14 @@ theorem unaryPair_square_cleanup_step (true :: base) [] output []) = some (unaryPairConfiguration 10 [] [] [] [] [] base [] output []) := by - unaryPairStepTac + unaryPairStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem unaryPair_square_cleanup_finish (output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 10 [] [] [] [] [] [] [] output []) = some (Turing.haltList actualUnaryPairIndexMachine output) := by - unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_input_step (bit : Bool) @@ -1701,7 +1712,7 @@ theorem unaryPair_failure_input_step first second matchedFirst matchedSecond base outer [] scratch) = some (unaryPairConfiguration 11 input first second matchedFirst matchedSecond base outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_first_step (bit : Bool) @@ -1713,7 +1724,7 @@ theorem unaryPair_failure_first_step base outer [] scratch) = some (unaryPairConfiguration 11 [] first second matchedFirst matchedSecond base outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_second_step (bit : Bool) @@ -1725,7 +1736,7 @@ theorem unaryPair_failure_second_step base outer [] scratch) = some (unaryPairConfiguration 11 [] [] second matchedFirst matchedSecond base outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_matchedFirst_step (bit : Bool) @@ -1736,7 +1747,7 @@ theorem unaryPair_failure_matchedFirst_step base outer [] scratch) = some (unaryPairConfiguration 11 [] [] [] matchedFirst matchedSecond base outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_matchedSecond_step (bit : Bool) @@ -1746,7 +1757,7 @@ theorem unaryPair_failure_matchedSecond_step (bit :: matchedSecond) base outer [] scratch) = some (unaryPairConfiguration 11 [] [] [] [] matchedSecond base outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_base_step (bit : Bool) (base outer scratch : List Bool) : @@ -1755,7 +1766,7 @@ theorem unaryPair_failure_base_step (bit :: base) outer [] scratch) = some (unaryPairConfiguration 11 [] [] [] [] [] base outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_outer_step (bit : Bool) (outer scratch : List Bool) : @@ -1764,7 +1775,7 @@ theorem unaryPair_failure_outer_step (bit :: outer) [] scratch) = some (unaryPairConfiguration 11 [] [] [] [] [] [] outer [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_scratch_step (bit : Bool) (scratch : List Bool) : @@ -1773,13 +1784,13 @@ theorem unaryPair_failure_scratch_step [] (bit :: scratch)) = some (unaryPairConfiguration 11 [] [] [] [] [] [] [] [] scratch) := by - cases bit <;> unaryPairStepTac + unaryPairStepOnly theorem unaryPair_failure_finish : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] [] [] [] [] [] []) = some (Turing.haltList actualUnaryPairIndexMachine []) := by - unaryPairStepTac + unaryPairStepOnly end CNFUnaryPairIndexTM diff --git a/LeanPool/GapCVP/Part05A.lean b/LeanPool/GapCVP/Part05A.lean index 3b2df62b2a..bca13da858 100644 --- a/LeanPool/GapCVP/Part05A.lean +++ b/LeanPool/GapCVP/Part05A.lean @@ -617,6 +617,16 @@ macro "sourcePairPrefixStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a source pair prefix step using the fixed simplification rules. -/ +macro "sourcePairPrefixStepOnly" : tactic => + `(tactic| machineStackEquality [ + actualSourcePairPrefixMachine, sourcePairPrefixConfiguration, sourcePairPrefixPeek, + sourcePairPrefixPop, sourcePairPrefixPush, sourcePairPrefixGoto, + sourcePairPrefixFirstStatement, sourcePairPrefixSecondStatement, + sourcePairPrefixSuffixStatement, sourcePairPrefixSecondRestoreStatement, + sourcePairPrefixFirstRestoreStatement, sourcePairPrefixFailureStatement, Turing.haltList, + Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_first_true (input first second output : List Bool) : @@ -625,7 +635,7 @@ theorem sourcePairPrefix_first_true (true :: input) first second output) = some (sourcePairPrefixConfiguration 0 input (true :: first) second output) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_first_false @@ -635,7 +645,7 @@ theorem sourcePairPrefix_first_false (false :: input) first second output) = some (sourcePairPrefixConfiguration 1 input first second output) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_first_missing @@ -643,7 +653,7 @@ theorem sourcePairPrefix_first_missing actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 [] first second output) = some (sourcePairPrefixConfiguration 5 [] first second output) := by - sourcePairPrefixStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_second_true @@ -653,7 +663,7 @@ theorem sourcePairPrefix_second_true (true :: input) first second output) = some (sourcePairPrefixConfiguration 1 input first (true :: second) output) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_second_false @@ -663,7 +673,7 @@ theorem sourcePairPrefix_second_false (false :: input) first second output) = some (sourcePairPrefixConfiguration 2 input first second (false :: output)) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_second_missing @@ -671,7 +681,7 @@ theorem sourcePairPrefix_second_missing actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 [] first second output) = some (sourcePairPrefixConfiguration 5 [] first second output) := by - sourcePairPrefixStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_suffix_step @@ -681,7 +691,7 @@ theorem sourcePairPrefix_suffix_step (bit :: input) first second output) = some (sourcePairPrefixConfiguration 2 input first second output) := by - cases bit <;> sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_suffix_finish @@ -690,7 +700,7 @@ theorem sourcePairPrefix_suffix_finish (sourcePairPrefixConfiguration 2 [] first second output) = some (sourcePairPrefixConfiguration 3 [] first second output) := by - sourcePairPrefixStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_secondRestore_step @@ -700,7 +710,7 @@ theorem sourcePairPrefix_secondRestore_step [] first (true :: second) output) = some (sourcePairPrefixConfiguration 3 [] first second (true :: output)) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_secondRestore_finish @@ -709,7 +719,7 @@ theorem sourcePairPrefix_secondRestore_finish (sourcePairPrefixConfiguration 3 [] first [] output) = some (sourcePairPrefixConfiguration 4 [] first [] (false :: output)) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_firstRestore_step @@ -719,7 +729,7 @@ theorem sourcePairPrefix_firstRestore_step [] (true :: first) [] output) = some (sourcePairPrefixConfiguration 4 [] first [] (true :: output)) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_firstRestore_finish @@ -727,7 +737,7 @@ theorem sourcePairPrefix_firstRestore_finish actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 4 [] [] [] output) = some (Turing.haltList actualSourcePairPrefixMachine output) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_failure_input_step @@ -737,7 +747,7 @@ theorem sourcePairPrefix_failure_input_step (bit :: input) first second output) = some (sourcePairPrefixConfiguration 5 input first second output) := by - cases bit <;> sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_failure_first_step @@ -747,7 +757,7 @@ theorem sourcePairPrefix_failure_first_step [] (bit :: first) second output) = some (sourcePairPrefixConfiguration 5 [] first second output) := by - cases bit <;> sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_failure_second_step @@ -757,7 +767,7 @@ theorem sourcePairPrefix_failure_second_step [] [] (bit :: second) output) = some (sourcePairPrefixConfiguration 5 [] [] second output) := by - cases bit <;> sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_failure_output_step @@ -765,14 +775,14 @@ theorem sourcePairPrefix_failure_output_step actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] [] (bit :: output)) = some (sourcePairPrefixConfiguration 5 [] [] [] output) := by - cases bit <;> sourcePairPrefixStepTac + sourcePairPrefixStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourcePairPrefix_failure_finish : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] [] []) = some (Turing.haltList actualSourcePairPrefixMachine []) := by - sourcePairPrefixStepTac + sourcePairPrefixStepOnly end CNFSourcePairPrefixWorkerTM diff --git a/LeanPool/GapCVP/Part05B.lean b/LeanPool/GapCVP/Part05B.lean index ae20448d40..f59c88726e 100644 --- a/LeanPool/GapCVP/Part05B.lean +++ b/LeanPool/GapCVP/Part05B.lean @@ -463,7 +463,7 @@ private theorem formulaPreservation_copy_step (bit : Bool) some (formulaPreservationConfiguration 17 input counter field binary borrow output (bit :: backup) (bit :: scratch)) := by - cases bit <;> formulaPreservationStepTac + reduceMachineConfiguration [formulaPreservationConfiguration] (formulaPreservationStepTac) private theorem formulaPreservation_copy_finish (counter field binary borrow output backup scratch : List Bool) : @@ -472,7 +472,7 @@ private theorem formulaPreservation_copy_finish [] counter field binary borrow output backup scratch) = some (formulaPreservationConfiguration 18 [] counter field binary borrow output backup scratch) := by - formulaPreservationStepTac + rfl private theorem formulaPreservation_restore_step (bit : Bool) (input counter field binary borrow output backup scratch : List Bool) : @@ -482,7 +482,7 @@ private theorem formulaPreservation_restore_step (bit : Bool) (bit :: scratch)) = some (formulaPreservationConfiguration 18 (bit :: input) counter field binary borrow output backup scratch) := by - cases bit <;> formulaPreservationStepTac + reduceMachineConfiguration [formulaPreservationConfiguration] (formulaPreservationStepTac) private theorem formulaPreservation_restore_finish (input counter field binary borrow output backup : List Bool) : @@ -491,7 +491,7 @@ private theorem formulaPreservation_restore_finish input counter field binary borrow output backup []) = some (formulaPreservationConfiguration 0 input counter field binary borrow output backup []) := by - formulaPreservationStepTac + rfl private theorem formulaPreservation_output_step (bit : Bool) (input counter field binary borrow output backup scratch : List Bool) : @@ -502,14 +502,14 @@ private theorem formulaPreservation_output_step (bit : Bool) some (formulaPreservationConfiguration 19 input counter field binary borrow (bit :: output) backup scratch) := by - cases bit <;> formulaPreservationStepTac + reduceMachineConfiguration [formulaPreservationConfiguration] (formulaPreservationStepTac) private theorem formulaPreservation_output_finish (output : List Bool) : formulaPreservationMachine.step (formulaPreservationConfiguration 19 [] [] [] [] [] output [] []) = some (Turing.haltList formulaPreservationMachine output) := by - formulaPreservationStepTac + reduceMachineConfiguration [formulaPreservationConfiguration] (formulaPreservationStepTac) private def formulaPreservationCanonicalStacks (source : (stack : Fin 6) → List Bool) @@ -904,6 +904,13 @@ macro "sourceMarkerStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a source marker step using the fixed simplification rules. -/ +macro "sourceMarkerStepOnly" : tactic => + `(tactic| machineStackEquality [ + sourceMarkerRotationMachine, sourceMarkerConfiguration, sourceMarkerPeek, sourceMarkerPop, + sourceMarkerPush, sourceMarkerGoto, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + private theorem sourceMarker_copy_step (bit : Bool) (input scratch output : List Bool) : sourceMarkerRotationMachine.step @@ -911,27 +918,27 @@ private theorem sourceMarker_copy_step (bit : Bool) (bit :: input) scratch output) = some (sourceMarkerConfiguration 0 input (bit :: scratch) output) := by - cases bit <;> sourceMarkerStepTac + sourceMarkerStepOnly private theorem sourceMarker_copy_finish (scratch output : List Bool) : sourceMarkerRotationMachine.step (sourceMarkerConfiguration 0 [] scratch output) = some (sourceMarkerConfiguration 1 [] scratch output) := by - sourceMarkerStepTac + rfl private theorem sourceMarker_extract_step (bit : Bool) (scratch output : List Bool) : sourceMarkerRotationMachine.step (sourceMarkerConfiguration 1 [] (bit :: scratch) output) = some (sourceMarkerConfiguration 2 [bit] scratch output) := by - cases bit <;> sourceMarkerStepTac + sourceMarkerStepOnly private theorem sourceMarker_extract_missing (output : List Bool) : sourceMarkerRotationMachine.step (sourceMarkerConfiguration 1 [] [] output) = some (sourceMarkerConfiguration 2 [false] [] output) := by - sourceMarkerStepTac + sourceMarkerStepOnly private theorem sourceMarker_restore_step (bit : Bool) (input scratch output : List Bool) : @@ -940,14 +947,14 @@ private theorem sourceMarker_restore_step (bit : Bool) input (bit :: scratch) output) = some (sourceMarkerConfiguration 2 input scratch (bit :: output)) := by - cases bit <;> sourceMarkerStepTac + sourceMarkerStepOnly private theorem sourceMarker_restore_finish (input output : List Bool) : sourceMarkerRotationMachine.step (sourceMarkerConfiguration 2 input [] output) = some (sourceMarkerConfiguration 3 input [] output) := by - sourceMarkerStepTac + rfl private theorem sourceMarker_output_finish (bit : Bool) (output : List Bool) : @@ -955,7 +962,7 @@ private theorem sourceMarker_output_finish (bit : Bool) (sourceMarkerConfiguration 3 [bit] [] output) = some (Turing.haltList sourceMarkerRotationMachine (bit :: output)) := by - cases bit <;> sourceMarkerStepTac + sourceMarkerStepOnly private def sourceMarker_copyTrace (input scratch output : List Bool) : @@ -1253,11 +1260,20 @@ macro "radiusMarkerTailStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a radius marker tail step using the fixed simplification rules. -/ +macro "radiusMarkerTailStepOnly" : tactic => + `(tactic| machineStackEquality [ + radiusMarkerTailMachine, radiusMarkerTailConfiguration, radiusMarkerTailPeek, + radiusMarkerTailPop, radiusMarkerTailPush, radiusMarkerTailGoto, + radiusMarkerTailDropStatement, radiusMarkerTailCopyStatement, + radiusMarkerTailOutputStatement, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + private theorem radiusMarkerTail_empty_finish : radiusMarkerTailMachine.step (radiusMarkerTailConfiguration 0 [] [] []) = some (Turing.haltList radiusMarkerTailMachine []) := by - radiusMarkerTailStepTac + radiusMarkerTailStepOnly private theorem radiusMarkerTail_drop_step (bit : Bool) (input scratch output : List Bool) : @@ -1266,7 +1282,7 @@ private theorem radiusMarkerTail_drop_step (bit : Bool) (bit :: input) scratch output) = some (radiusMarkerTailConfiguration 1 input scratch output) := by - cases bit <;> radiusMarkerTailStepTac + radiusMarkerTailStepOnly private theorem radiusMarkerTail_copy_step (bit : Bool) (input scratch output : List Bool) : @@ -1275,14 +1291,14 @@ private theorem radiusMarkerTail_copy_step (bit : Bool) (bit :: input) scratch output) = some (radiusMarkerTailConfiguration 1 input (bit :: scratch) output) := by - cases bit <;> radiusMarkerTailStepTac + radiusMarkerTailStepOnly private theorem radiusMarkerTail_copy_finish (scratch output : List Bool) : radiusMarkerTailMachine.step (radiusMarkerTailConfiguration 1 [] scratch output) = some (radiusMarkerTailConfiguration 2 [] scratch output) := by - radiusMarkerTailStepTac + rfl private theorem radiusMarkerTail_output_step (bit : Bool) (scratch output : List Bool) : @@ -1291,13 +1307,13 @@ private theorem radiusMarkerTail_output_step (bit : Bool) [] (bit :: scratch) output) = some (radiusMarkerTailConfiguration 2 [] scratch (bit :: output)) := by - cases bit <;> radiusMarkerTailStepTac + radiusMarkerTailStepOnly private theorem radiusMarkerTail_output_finish (output : List Bool) : radiusMarkerTailMachine.step (radiusMarkerTailConfiguration 2 [] [] output) = some (Turing.haltList radiusMarkerTailMachine output) := by - radiusMarkerTailStepTac + radiusMarkerTailStepOnly private def radiusMarkerTail_copyTrace (input scratch output : List Bool) : @@ -1516,6 +1532,14 @@ macro "rationalRadiusStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a rational radius step using the fixed simplification rules. -/ +macro "rationalRadiusStepOnly" : tactic => + `(tactic| machineStackEquality [ + rationalRadiusMachine, rationalRadiusConfiguration, rationalRadiusFailureStatement, + normalizedRadiusPeek, normalizedRadiusPop, normalizedRadiusPush, normalizedRadiusGoto, + normalizedRadiusFailureCheck, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_marker_true_step (input base outer restore output : List Bool) : @@ -1524,7 +1548,7 @@ theorem rationalRadius_marker_true_step (true :: input) base outer restore output) = some (rationalRadiusConfiguration 1 input base outer restore (true :: output)) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_marker_false_step @@ -1534,7 +1558,7 @@ theorem rationalRadius_marker_false_step (false :: input) base outer restore output) = some (rationalRadiusConfiguration 6 input base outer restore output) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_marker_missing_step @@ -1544,7 +1568,7 @@ theorem rationalRadius_marker_missing_step base outer restore output) = some (rationalRadiusConfiguration 6 [] base outer restore output) := by - rationalRadiusStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_scan_true_step @@ -1556,7 +1580,7 @@ theorem rationalRadius_scan_true_step (true :: true :: base) (true :: true :: outer) restore (true :: true :: output)) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_scan_false_step @@ -1566,7 +1590,7 @@ theorem rationalRadius_scan_false_step (false :: input) base outer restore output) = some (rationalRadiusConfiguration 6 input base outer restore output) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_scan_finish @@ -1576,7 +1600,7 @@ theorem rationalRadius_scan_finish base outer restore output) = some (rationalRadiusConfiguration 2 [] base outer restore output) := by - rationalRadiusStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_outer_step @@ -1586,7 +1610,7 @@ theorem rationalRadius_outer_step base (true :: outer) restore output) = some (rationalRadiusConfiguration 3 [] base outer restore output) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_outer_finish @@ -1596,7 +1620,7 @@ theorem rationalRadius_outer_finish base [] restore output) = some (rationalRadiusConfiguration 5 [] base [] restore output) := by - rationalRadiusStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_copy_step @@ -1606,7 +1630,7 @@ theorem rationalRadius_copy_step (true :: base) outer restore output) = some (rationalRadiusConfiguration 3 [] base outer (true :: restore) (true :: output)) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_copy_finish @@ -1616,7 +1640,7 @@ theorem rationalRadius_copy_finish [] outer restore output) = some (rationalRadiusConfiguration 4 [] [] outer restore output) := by - rationalRadiusStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_restore_step @@ -1626,7 +1650,7 @@ theorem rationalRadius_restore_step base outer (true :: restore) output) = some (rationalRadiusConfiguration 4 [] (true :: base) outer restore output) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_restore_finish @@ -1636,7 +1660,7 @@ theorem rationalRadius_restore_finish base outer [] output) = some (rationalRadiusConfiguration 2 [] base outer [] output) := by - rationalRadiusStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_cleanup_base_step @@ -1646,7 +1670,7 @@ theorem rationalRadius_cleanup_base_step (true :: base) [] [] output) = some (rationalRadiusConfiguration 5 [] base [] [] output) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_cleanup_finish (output : List Bool) : @@ -1654,7 +1678,7 @@ theorem rationalRadius_cleanup_finish (output : List Bool) : (rationalRadiusConfiguration 5 [] [] [] [] output) = some (Turing.haltList rationalRadiusMachine (true :: output)) := by - rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_failure_input_step @@ -1664,7 +1688,7 @@ theorem rationalRadius_failure_input_step (bit :: input) base outer restore output) = some (rationalRadiusConfiguration 6 input base outer restore output) := by - cases bit <;> rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_failure_base_step @@ -1674,7 +1698,7 @@ theorem rationalRadius_failure_base_step (bit :: base) outer restore output) = some (rationalRadiusConfiguration 6 [] base outer restore output) := by - cases bit <;> rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_failure_outer_step @@ -1684,7 +1708,7 @@ theorem rationalRadius_failure_outer_step (bit :: outer) restore output) = some (rationalRadiusConfiguration 6 [] [] outer restore output) := by - cases bit <;> rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_failure_restore_step @@ -1694,7 +1718,7 @@ theorem rationalRadius_failure_restore_step (bit :: restore) output) = some (rationalRadiusConfiguration 6 [] [] [] restore output) := by - cases bit <;> rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_failure_output_step @@ -1703,14 +1727,14 @@ theorem rationalRadius_failure_output_step (rationalRadiusConfiguration 6 [] [] [] [] (bit :: output)) = some (rationalRadiusConfiguration 6 [] [] [] [] output) := by - cases bit <;> rationalRadiusStepTac + rationalRadiusStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem rationalRadius_failure_finish : rationalRadiusMachine.step (rationalRadiusConfiguration 6 [] [] [] [] []) = some (Turing.haltList rationalRadiusMachine [false]) := by - rationalRadiusStepTac + rationalRadiusStepOnly end SourceLatticeStructuralRationalRadiusTM diff --git a/LeanPool/GapCVP/Part05C.lean b/LeanPool/GapCVP/Part05C.lean index c98f6f2552..4dfbf1bc04 100644 --- a/LeanPool/GapCVP/Part05C.lean +++ b/LeanPool/GapCVP/Part05C.lean @@ -434,8 +434,7 @@ theorem readUnaryPrefix_none_eq_replicate cases hrest : readUnaryPrefix rest with | none => have htail := ih hrest - simpa only [List.length_cons, List.replicate_succ] - using congrArg (fun tail : List Bool => true :: tail) htail + exact congrArg (fun tail : List Bool => true :: tail) htail | some pair => simp only [readUnaryPrefix, hrest, reduceCtorEq] at hread @@ -817,6 +816,16 @@ macro "sourceFlatAtomicStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a source flat atomic step using the fixed simplification rules. -/ +macro "sourceFlatAtomicStepOnly" : tactic => + `(tactic| machineStackEquality [ + sourceFlatAtomicRecordMachine, sourceFlatAtomicConfiguration, sourceFlatAtomicPeek, + sourceFlatAtomicPop, sourceFlatAtomicPushBit, sourceFlatAtomicPushConstant, + sourceFlatAtomicGoto, sourceFlatAtomicPrefixStatement, sourceFlatAtomicPayloadStatement, + sourceFlatAtomicPayloadOutputStatement, sourceFlatAtomicPendingStatement, + sourceFlatAtomicRestoreStatement, sourceFlatAtomicFailureStatement, Turing.haltList, + Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + private theorem sourceFlatAtomic_prefix_true (input counter payload pending output : List Bool) : sourceFlatAtomicRecordMachine.step @@ -824,7 +833,7 @@ private theorem sourceFlatAtomic_prefix_true (true :: input) counter payload pending output) = some (sourceFlatAtomicConfiguration 0 input (true :: counter) payload pending output) := by - sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_prefix_delimiter (input counter payload pending output : List Bool) : @@ -833,7 +842,7 @@ private theorem sourceFlatAtomic_prefix_delimiter (false :: input) counter payload pending output) = some (sourceFlatAtomicConfiguration 1 input counter payload pending output) := by - sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_prefix_missing (counter payload pending output : List Bool) : @@ -842,7 +851,7 @@ private theorem sourceFlatAtomic_prefix_missing [] counter payload pending output) = some (sourceFlatAtomicConfiguration 5 [] counter payload pending output) := by - sourceFlatAtomicStepTac + rfl private theorem sourceFlatAtomic_payload_step (bit : Bool) (input counter payload pending output : List Bool) : @@ -852,7 +861,7 @@ private theorem sourceFlatAtomic_payload_step payload pending output) = some (sourceFlatAtomicConfiguration 1 input counter (bit :: payload) pending output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_payload_missing (counter payload pending output : List Bool) : @@ -861,7 +870,7 @@ private theorem sourceFlatAtomic_payload_missing [] (true :: counter) payload pending output) = some (sourceFlatAtomicConfiguration 5 [] counter payload pending output) := by - sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_payload_finish (input payload pending output : List Bool) : @@ -870,7 +879,7 @@ private theorem sourceFlatAtomic_payload_finish input [] payload pending output) = some (sourceFlatAtomicConfiguration 2 input [] payload pending output) := by - sourceFlatAtomicStepTac + rfl private theorem sourceFlatAtomic_payload_output_step (bit : Bool) (input payload pending output : List Bool) : @@ -879,7 +888,7 @@ private theorem sourceFlatAtomic_payload_output_step input [] (bit :: payload) pending output) = some (sourceFlatAtomicConfiguration 2 input [] payload pending (bit :: output)) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_payload_output_finish (input pending output : List Bool) : @@ -888,7 +897,7 @@ private theorem sourceFlatAtomic_payload_output_finish input [] [] pending output) = some (sourceFlatAtomicConfiguration 3 input [] [] pending output) := by - sourceFlatAtomicStepTac + rfl private theorem sourceFlatAtomic_pending_step (bit : Bool) (input pending output : List Bool) : @@ -897,7 +906,7 @@ private theorem sourceFlatAtomic_pending_step (bit :: input) [] [] pending output) = some (sourceFlatAtomicConfiguration 3 input [] [] (bit :: pending) output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_pending_finish (pending output : List Bool) : @@ -906,7 +915,7 @@ private theorem sourceFlatAtomic_pending_finish [] [] [] pending output) = some (sourceFlatAtomicConfiguration 4 [] [] [] pending output) := by - sourceFlatAtomicStepTac + rfl private theorem sourceFlatAtomic_restore_step (bit : Bool) (pending output : List Bool) : @@ -915,13 +924,13 @@ private theorem sourceFlatAtomic_restore_step [] [] [] (bit :: pending) output) = some (sourceFlatAtomicConfiguration 4 [] [] [] pending (bit :: output)) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_restore_finish (output : List Bool) : sourceFlatAtomicRecordMachine.step (sourceFlatAtomicConfiguration 4 [] [] [] [] output) = some (Turing.haltList sourceFlatAtomicRecordMachine output) := by - sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_failure_input_step (bit : Bool) (input counter payload pending output : List Bool) : @@ -930,7 +939,7 @@ private theorem sourceFlatAtomic_failure_input_step (bit :: input) counter payload pending output) = some (sourceFlatAtomicConfiguration 5 input counter payload pending output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_failure_counter_step (bit : Bool) (counter payload pending output : List Bool) : @@ -939,7 +948,7 @@ private theorem sourceFlatAtomic_failure_counter_step [] (bit :: counter) payload pending output) = some (sourceFlatAtomicConfiguration 5 [] counter payload pending output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_failure_payload_step (bit : Bool) (payload pending output : List Bool) : @@ -948,7 +957,7 @@ private theorem sourceFlatAtomic_failure_payload_step [] [] (bit :: payload) pending output) = some (sourceFlatAtomicConfiguration 5 [] [] payload pending output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_failure_pending_step (bit : Bool) (pending output : List Bool) : @@ -957,7 +966,7 @@ private theorem sourceFlatAtomic_failure_pending_step [] [] [] (bit :: pending) output) = some (sourceFlatAtomicConfiguration 5 [] [] [] pending output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_failure_output_step (bit : Bool) (output : List Bool) : @@ -966,13 +975,13 @@ private theorem sourceFlatAtomic_failure_output_step [] [] [] [] (bit :: output)) = some (sourceFlatAtomicConfiguration 5 [] [] [] [] output) := by - cases bit <;> sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private theorem sourceFlatAtomic_failure_finish : sourceFlatAtomicRecordMachine.step (sourceFlatAtomicConfiguration 5 [] [] [] [] []) = some (Turing.haltList sourceFlatAtomicRecordMachine []) := by - sourceFlatAtomicStepTac + sourceFlatAtomicStepOnly private def sourceFlatAtomicFailureBudget (input counter payload pending output : List Bool) : ℕ := @@ -1589,6 +1598,17 @@ macro "sourceGridIndexStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a source grid index step using the fixed simplification rules. -/ +macro "sourceGridIndexStepOnly" : tactic => + `(tactic| machineStackEquality [ + sourceCanonicalUnaryGridIndexMachine, sourceGridIndexConfiguration, sourceGridIndexPeek, + sourceGridIndexPop, sourceGridIndexPushBit, sourceGridIndexPushConstant, + sourceGridIndexGoto, sourceGridIndexPrefixStatement, sourceGridIndexArchiveStatement, + sourceGridIndexSourceRestoreStatement, sourceGridIndexOuterStatement, + sourceGridIndexCopyStatement, sourceGridIndexTemplateRestoreStatement, + sourceGridIndexFailureStatement, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_prefix_true (input counter scratch archive output : List Bool) : @@ -1597,7 +1617,7 @@ theorem sourceGridIndex_prefix_true (true :: input) counter scratch archive output) = some (sourceGridIndexConfiguration 0 input (true :: counter) scratch archive output) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_prefix_false @@ -1607,7 +1627,7 @@ theorem sourceGridIndex_prefix_false (false :: input) counter scratch archive output) = some (sourceGridIndexConfiguration 1 input counter scratch archive output) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_prefix_missing @@ -1617,7 +1637,7 @@ theorem sourceGridIndex_prefix_missing [] counter scratch archive output) = some (sourceGridIndexConfiguration 6 [] counter scratch archive output) := by - sourceGridIndexStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_archive_step @@ -1627,7 +1647,7 @@ theorem sourceGridIndex_archive_step (bit :: input) counter scratch archive output) = some (sourceGridIndexConfiguration 1 input counter scratch (bit :: archive) output) := by - cases bit <;> sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_archive_finish @@ -1637,7 +1657,7 @@ theorem sourceGridIndex_archive_finish [] counter scratch archive output) = some (sourceGridIndexConfiguration 2 [] counter scratch archive output) := by - sourceGridIndexStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_source_restore_step @@ -1647,7 +1667,7 @@ theorem sourceGridIndex_source_restore_step [] counter scratch (bit :: archive) output) = some (sourceGridIndexConfiguration 2 [] counter scratch archive (bit :: output)) := by - cases bit <;> sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_source_restore_finish @@ -1657,7 +1677,7 @@ theorem sourceGridIndex_source_restore_finish [] counter scratch [] output) = some (sourceGridIndexConfiguration 3 [] counter scratch [] output) := by - sourceGridIndexStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_outer_step @@ -1667,7 +1687,7 @@ theorem sourceGridIndex_outer_step [] (true :: counter) [] [] output) = some (sourceGridIndexConfiguration 4 [] counter [] [] output) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_outer_finish (output : List Bool) : @@ -1675,7 +1695,7 @@ theorem sourceGridIndex_outer_finish (output : List Bool) : (sourceGridIndexConfiguration 3 [] [] [] [] output) = some (Turing.haltList sourceCanonicalUnaryGridIndexMachine output) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_copy_step @@ -1685,7 +1705,7 @@ theorem sourceGridIndex_copy_step [] (true :: counter) scratch [] output) = some (sourceGridIndexConfiguration 4 [] counter (true :: scratch) [] (true :: output)) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_copy_finish @@ -1695,7 +1715,7 @@ theorem sourceGridIndex_copy_finish [] [] scratch [] output) = some (sourceGridIndexConfiguration 5 [] [] scratch [] (false :: output)) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_template_restore_step @@ -1705,7 +1725,7 @@ theorem sourceGridIndex_template_restore_step [] counter (true :: scratch) [] output) = some (sourceGridIndexConfiguration 5 [] (true :: counter) scratch [] (true :: output)) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_template_restore_finish @@ -1715,7 +1735,7 @@ theorem sourceGridIndex_template_restore_finish [] counter [] [] output) = some (sourceGridIndexConfiguration 3 [] counter [] [] output) := by - sourceGridIndexStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_failure_step @@ -1725,7 +1745,7 @@ theorem sourceGridIndex_failure_step [] (true :: counter) [] [] []) = some (sourceGridIndexConfiguration 6 [] counter [] [] []) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceGridIndex_failure_finish : @@ -1733,7 +1753,7 @@ theorem sourceGridIndex_failure_finish : (sourceGridIndexConfiguration 6 [] [] [] [] []) = some (Turing.haltList sourceCanonicalUnaryGridIndexMachine []) := by - sourceGridIndexStepTac + sourceGridIndexStepOnly end SourceCanonicalUnaryGridIndexTM diff --git a/LeanPool/GapCVP/Part05D.lean b/LeanPool/GapCVP/Part05D.lean index 3d6d9b0954..bddbd0025e 100644 --- a/LeanPool/GapCVP/Part05D.lean +++ b/LeanPool/GapCVP/Part05D.lean @@ -925,7 +925,7 @@ private theorem originalSourcePreserving_copy_step computer 0 input (bit :: backup) (bit :: scratch) result) := by classical - cases bit <;> originalSourcePreservationStepTac + originalSourcePreservationStepTac private theorem originalSourcePreserving_copy_finish {f : List Bool → List Bool} @@ -950,7 +950,7 @@ private theorem originalSourcePreserving_input_restore_step some (originalSourceCopyConfiguration computer 1 (bit :: input) backup scratch result) := by classical - cases bit <;> originalSourcePreservationStepTac + originalSourcePreservationStepTac private theorem originalSourcePreserving_input_restore_finish {f : List Bool → List Bool} @@ -977,7 +977,7 @@ private theorem originalSourcePreserving_output_archive_step some (originalSourceOutputConfiguration computer 2 output backup scratch (bit :: result)) := by classical - cases bit <;> originalSourcePreservationStepTac + originalSourcePreservationStepTac private theorem originalSourcePreserving_output_archive_finish {f : List Bool → List Bool} @@ -1002,7 +1002,7 @@ private theorem originalSourcePreserving_source_restore_step some (originalSourceOutputConfiguration computer 3 (bit :: output) backup [] result) := by classical - cases bit <;> originalSourcePreservationStepTac + originalSourcePreservationStepTac private theorem originalSourcePreserving_source_restore_finish {f : List Bool → List Bool} @@ -1027,7 +1027,7 @@ private theorem originalSourcePreserving_result_restore_step some (originalSourceOutputConfiguration computer 4 (bit :: output) [] [] result) := by classical - cases bit <;> originalSourcePreservationStepTac + originalSourcePreservationStepTac private theorem originalSourcePreserving_result_restore_finish {f : List Bool → List Bool} @@ -1565,6 +1565,18 @@ macro "flatAdjacentRecordStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a flat adjacent record step using the fixed simplification rules. -/ +macro "flatAdjacentRecordStepOnly" : tactic => + `(tactic| machineStackEquality [ + actualFlatAdjacentRecordSwapMachine, flatAdjacentRecordConfiguration, + flatAdjacentRecordPeek, flatAdjacentRecordPop, flatAdjacentRecordPushBit, + flatAdjacentRecordPushConstant, flatAdjacentRecordGoto, + flatAdjacentRecordFirstPrefixStatement, flatAdjacentRecordFirstPayloadStatement, + flatAdjacentRecordSecondPrefixStatement, flatAdjacentRecordSecondPayloadStatement, + flatAdjacentRecordRestoreFirstStatement, flatAdjacentRecordRestoreSecondStatement, + flatAdjacentRecordFailureStatement, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_firstPrefix_true (input first second counter : List Bool) : @@ -1573,7 +1585,7 @@ theorem flatAdjacentRecord_firstPrefix_true (true :: input) first second counter) = some (flatAdjacentRecordConfiguration 0 input (true :: first) second (true :: counter)) := by - flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_firstPrefix_false @@ -1583,7 +1595,7 @@ theorem flatAdjacentRecord_firstPrefix_false (false :: input) first second counter) = some (flatAdjacentRecordConfiguration 1 input (false :: first) second counter) := by - flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_firstPrefix_missing @@ -1592,7 +1604,7 @@ theorem flatAdjacentRecord_firstPrefix_missing (flatAdjacentRecordConfiguration 0 [] first second counter) = some (flatAdjacentRecordConfiguration 6 [] first second counter) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_firstPayload_step @@ -1602,7 +1614,7 @@ theorem flatAdjacentRecord_firstPayload_step (bit :: input) first second (true :: counter)) = some (flatAdjacentRecordConfiguration 1 input (bit :: first) second counter) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_firstPayload_missing @@ -1612,7 +1624,7 @@ theorem flatAdjacentRecord_firstPayload_missing [] first second (true :: counter)) = some (flatAdjacentRecordConfiguration 6 [] first second (true :: counter)) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_firstPayload_finish @@ -1620,7 +1632,7 @@ theorem flatAdjacentRecord_firstPayload_finish actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 1 input first second []) = some (flatAdjacentRecordConfiguration 2 input first second []) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_secondPrefix_true @@ -1630,7 +1642,7 @@ theorem flatAdjacentRecord_secondPrefix_true (true :: input) first second counter) = some (flatAdjacentRecordConfiguration 2 input first (true :: second) (true :: counter)) := by - flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_secondPrefix_false @@ -1640,7 +1652,7 @@ theorem flatAdjacentRecord_secondPrefix_false (false :: input) first second counter) = some (flatAdjacentRecordConfiguration 3 input first (false :: second) counter) := by - flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_secondPrefix_missing @@ -1649,7 +1661,7 @@ theorem flatAdjacentRecord_secondPrefix_missing (flatAdjacentRecordConfiguration 2 [] first second counter) = some (flatAdjacentRecordConfiguration 6 [] first second counter) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_secondPayload_step @@ -1659,7 +1671,7 @@ theorem flatAdjacentRecord_secondPayload_step (bit :: input) first second (true :: counter)) = some (flatAdjacentRecordConfiguration 3 input first (bit :: second) counter) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_secondPayload_missing @@ -1669,7 +1681,7 @@ theorem flatAdjacentRecord_secondPayload_missing [] first second (true :: counter)) = some (flatAdjacentRecordConfiguration 6 [] first second (true :: counter)) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_secondPayload_finish @@ -1677,7 +1689,7 @@ theorem flatAdjacentRecord_secondPayload_finish actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 3 input first second []) = some (flatAdjacentRecordConfiguration 4 input first second []) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_restoreFirst_step @@ -1687,7 +1699,7 @@ theorem flatAdjacentRecord_restoreFirst_step input (bit :: first) second []) = some (flatAdjacentRecordConfiguration 4 (bit :: input) first second []) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_restoreFirst_finish @@ -1695,7 +1707,7 @@ theorem flatAdjacentRecord_restoreFirst_finish actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 4 input [] second []) = some (flatAdjacentRecordConfiguration 5 input [] second []) := by - flatAdjacentRecordStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_restoreSecond_step @@ -1705,7 +1717,7 @@ theorem flatAdjacentRecord_restoreSecond_step input [] (bit :: second) []) = some (flatAdjacentRecordConfiguration 5 (bit :: input) [] second []) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_restoreSecond_finish @@ -1713,7 +1725,7 @@ theorem flatAdjacentRecord_restoreSecond_finish actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 5 input [] [] []) = some (Turing.haltList actualFlatAdjacentRecordSwapMachine input) := by - flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_failure_input @@ -1723,7 +1735,7 @@ theorem flatAdjacentRecord_failure_input (bit :: input) first second counter) = some (flatAdjacentRecordConfiguration 6 input first second counter) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_failure_first @@ -1733,7 +1745,7 @@ theorem flatAdjacentRecord_failure_first [] (bit :: first) second counter) = some (flatAdjacentRecordConfiguration 6 [] first second counter) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_failure_second @@ -1743,7 +1755,7 @@ theorem flatAdjacentRecord_failure_second [] [] (bit :: second) counter) = some (flatAdjacentRecordConfiguration 6 [] [] second counter) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_failure_counter @@ -1753,14 +1765,14 @@ theorem flatAdjacentRecord_failure_counter [] [] [] (bit :: counter)) = some (flatAdjacentRecordConfiguration 6 [] [] [] counter) := by - cases bit <;> flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem flatAdjacentRecord_failure_finish : actualFlatAdjacentRecordSwapMachine.step (flatAdjacentRecordConfiguration 6 [] [] [] []) = some (Turing.haltList actualFlatAdjacentRecordSwapMachine []) := by - flatAdjacentRecordStepTac + flatAdjacentRecordStepOnly end CNFFlatAdjacentRecordSwapTM diff --git a/LeanPool/GapCVP/Part05E.lean b/LeanPool/GapCVP/Part05E.lean index fac1519fcb..b1af2a2d45 100644 --- a/LeanPool/GapCVP/Part05E.lean +++ b/LeanPool/GapCVP/Part05E.lean @@ -988,6 +988,15 @@ macro "cappedUnaryMinimumStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a capped unary minimum step using the fixed simplification rules. -/ +macro "cappedUnaryMinimumStepOnly" : tactic => + `(tactic| machineStackEquality [ + actualCappedUnaryMinimumMachine, cappedUnaryMinimumConfiguration, cappedUnaryMinimumPeek, + cappedUnaryMinimumPop, cappedUnaryMinimumPush, cappedUnaryMinimumGoto, + cappedUnaryMinimumFirstStatement, cappedUnaryMinimumSecondStatement, + cappedUnaryMinimumSuccessStatement, cappedUnaryMinimumFailureStatement, Turing.haltList, + Turing.FinTM2.step, Turing.TM2.step, Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_first_true (input first output : List Bool) : @@ -996,7 +1005,7 @@ theorem cappedUnaryMinimum_first_true (true :: input) first output) = some (cappedUnaryMinimumConfiguration 0 input (true :: first) output) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_first_false @@ -1006,7 +1015,7 @@ theorem cappedUnaryMinimum_first_false (false :: input) first output) = some (cappedUnaryMinimumConfiguration 1 input first output) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_first_missing @@ -1015,7 +1024,7 @@ theorem cappedUnaryMinimum_first_missing (cappedUnaryMinimumConfiguration 0 [] first output) = some (cappedUnaryMinimumConfiguration 3 [] first output) := by - cappedUnaryMinimumStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_second_true_counter @@ -1025,7 +1034,7 @@ theorem cappedUnaryMinimum_second_true_counter (true :: input) (true :: first) output) = some (cappedUnaryMinimumConfiguration 1 input first (true :: output)) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_second_true_empty @@ -1035,7 +1044,7 @@ theorem cappedUnaryMinimum_second_true_empty (true :: input) [] output) = some (cappedUnaryMinimumConfiguration 1 input [] output) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_second_false @@ -1045,7 +1054,7 @@ theorem cappedUnaryMinimum_second_false (false :: input) first output) = some (cappedUnaryMinimumConfiguration 2 input first output) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_second_missing @@ -1054,7 +1063,7 @@ theorem cappedUnaryMinimum_second_missing (cappedUnaryMinimumConfiguration 1 [] first output) = some (cappedUnaryMinimumConfiguration 3 [] first output) := by - cappedUnaryMinimumStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_success_input @@ -1064,7 +1073,7 @@ theorem cappedUnaryMinimum_success_input (bit :: input) first output) = some (cappedUnaryMinimumConfiguration 2 input first output) := by - cases bit <;> cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_success_first @@ -1074,7 +1083,7 @@ theorem cappedUnaryMinimum_success_first [] (bit :: first) output) = some (cappedUnaryMinimumConfiguration 2 [] first output) := by - cases bit <;> cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_success_finish @@ -1083,7 +1092,7 @@ theorem cappedUnaryMinimum_success_finish (cappedUnaryMinimumConfiguration 2 [] [] output) = some (Turing.haltList actualCappedUnaryMinimumMachine output) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_failure_input @@ -1093,7 +1102,7 @@ theorem cappedUnaryMinimum_failure_input (bit :: input) first output) = some (cappedUnaryMinimumConfiguration 3 input first output) := by - cases bit <;> cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_failure_first @@ -1103,7 +1112,7 @@ theorem cappedUnaryMinimum_failure_first [] (bit :: first) output) = some (cappedUnaryMinimumConfiguration 3 [] first output) := by - cases bit <;> cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_failure_output @@ -1113,7 +1122,7 @@ theorem cappedUnaryMinimum_failure_output [] [] (bit :: output)) = some (cappedUnaryMinimumConfiguration 3 [] [] output) := by - cases bit <;> cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem cappedUnaryMinimum_failure_finish : @@ -1121,7 +1130,7 @@ theorem cappedUnaryMinimum_failure_finish : (cappedUnaryMinimumConfiguration 3 [] [] []) = some (Turing.haltList actualCappedUnaryMinimumMachine []) := by - cappedUnaryMinimumStepTac + cappedUnaryMinimumStepOnly end CNFCappedUnaryMinimumTM diff --git a/LeanPool/GapCVP/Part05F.lean b/LeanPool/GapCVP/Part05F.lean index 425ad6b23a..7ab29ad978 100644 --- a/LeanPool/GapCVP/Part05F.lean +++ b/LeanPool/GapCVP/Part05F.lean @@ -389,19 +389,19 @@ private theorem unaryPrefixSuffix_true_step (input : List Bool) : actualUnaryPrefixSuffixMachine.step (unaryPrefixSuffixConfiguration (true :: input)) = some (unaryPrefixSuffixConfiguration input) := by - compactMachineStepTac [actualUnaryPrefixSuffixMachine, unaryPrefixSuffixConfiguration] + rfl private theorem unaryPrefixSuffix_false_step (input : List Bool) : actualUnaryPrefixSuffixMachine.step (unaryPrefixSuffixConfiguration (false :: input)) = some (Turing.haltList actualUnaryPrefixSuffixMachine input) := by - compactMachineStepTac [actualUnaryPrefixSuffixMachine, unaryPrefixSuffixConfiguration] + rfl private theorem unaryPrefixSuffix_missing_step : actualUnaryPrefixSuffixMachine.step (unaryPrefixSuffixConfiguration []) = some (Turing.haltList actualUnaryPrefixSuffixMachine []) := by - compactMachineStepTac [actualUnaryPrefixSuffixMachine, unaryPrefixSuffixConfiguration] + rfl private def unaryPrefixSuffix_validTrace (count : ℕ) (suffix : List Bool) : diff --git a/LeanPool/GapCVP/Part06A.lean b/LeanPool/GapCVP/Part06A.lean index 544cfd3c0b..d30484479b 100644 --- a/LeanPool/GapCVP/Part06A.lean +++ b/LeanPool/GapCVP/Part06A.lean @@ -46,7 +46,7 @@ private theorem flatCappedUnarySourceListStep_iterate | cons head remaining ih => rw [List.length_cons, Function.iterate_succ_apply, flatCappedUnarySourceListStep_state] - simpa only [Nat.succ_eq_add_one, List.foldl_cons] using ih (min cap (Nat.succ (Nat.pair head + exact ih (min cap (Nat.succ (Nat.pair head accumulator))) private theorem flatCappedUnaryReverseFold_eq_source @@ -347,7 +347,7 @@ private theorem flatCappedUnarySourceListStep_pending rw [hshape] simp only [sourcePairPrefixOutput_pair, flatUnaryDropFields_two_unaryPair] - simpa [List.append_assoc] using + exact flatUnaryDropFields_six_unaryPairs cap cap first second next next suffix @@ -801,13 +801,13 @@ private theorem sourceInputErase_scan_step sourceInputEraseMachine.step (sourceInputEraseConfiguration (bit :: input)) = some (sourceInputEraseConfiguration input) := by - cases bit <;> compactMachineStepTac [sourceInputEraseMachine, sourceInputEraseConfiguration] + rfl private theorem sourceInputErase_finish : sourceInputEraseMachine.step (sourceInputEraseConfiguration []) = some (Turing.haltList sourceInputEraseMachine []) := by - compactMachineStepTac [sourceInputEraseMachine, sourceInputEraseConfiguration] + rfl private def sourceInputErase_totalTrace (input : List Bool) : EvalsToInTime sourceInputEraseMachine.step (sourceInputEraseConfiguration input) @@ -2223,6 +2223,23 @@ macro "sourceIntegerMultiplicationStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a source integer multiplication step using the fixed simplification rules. -/ +macro "sourceIntegerMultiplicationStepOnly" : tactic => + `(tactic| machineStackEquality [ + sourceUnaryIntegerMultiplicationMachine, sourceIntegerMultiplicationConfiguration, + sourceIntegerMultiplicationPeek, sourceIntegerMultiplicationPop, + sourceIntegerMultiplicationPush, sourceIntegerMultiplicationGoto, + sourceIntegerMultiplicationLeftStatement, sourceIntegerMultiplicationRightStatement, + sourceIntegerMultiplicationOuterStatement, sourceIntegerMultiplicationCopyStatement, + sourceIntegerMultiplicationRestoreStatement, + sourceIntegerMultiplicationSuccessCleanupStatement, + sourceIntegerMultiplicationFailureInputStatement, + sourceIntegerMultiplicationFailureLeftStatement, + sourceIntegerMultiplicationFailureRightStatement, + sourceIntegerMultiplicationFailureRestoreStatement, + sourceIntegerMultiplicationFailureOutputStatement, Turing.haltList, Turing.FinTM2.step, + Turing.TM2.step, Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_left_true (input left right restore output : List Bool) : @@ -2231,7 +2248,7 @@ theorem sourceIntegerMultiplication_left_true (true :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 0 input (true :: left) right restore output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_left_delimiter @@ -2241,7 +2258,7 @@ theorem sourceIntegerMultiplication_left_delimiter (false :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 1 input left right restore output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_left_missing @@ -2251,7 +2268,7 @@ theorem sourceIntegerMultiplication_left_missing [] left right restore output) = some (sourceIntegerMultiplicationConfiguration 6 [] left right restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_right_true @@ -2261,7 +2278,7 @@ theorem sourceIntegerMultiplication_right_true (true :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 1 input left (true :: right) restore output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_right_false @@ -2271,7 +2288,7 @@ theorem sourceIntegerMultiplication_right_false (false :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 6 input left right restore output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_right_finish @@ -2281,7 +2298,7 @@ theorem sourceIntegerMultiplication_right_finish [] left right restore output) = some (sourceIntegerMultiplicationConfiguration 2 [] left right restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_outer_step @@ -2291,7 +2308,7 @@ theorem sourceIntegerMultiplication_outer_step [] (true :: left) right restore output) = some (sourceIntegerMultiplicationConfiguration 3 [] left right restore output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_outer_finish @@ -2301,7 +2318,7 @@ theorem sourceIntegerMultiplication_outer_finish [] [] right restore output) = some (sourceIntegerMultiplicationConfiguration 5 [] [] right restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_copy_step @@ -2311,7 +2328,7 @@ theorem sourceIntegerMultiplication_copy_step [] left (true :: right) restore output) = some (sourceIntegerMultiplicationConfiguration 3 [] left right (true :: restore) (true :: output)) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_copy_finish @@ -2321,7 +2338,7 @@ theorem sourceIntegerMultiplication_copy_finish [] left [] restore output) = some (sourceIntegerMultiplicationConfiguration 4 [] left [] restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_restore_step @@ -2331,7 +2348,7 @@ theorem sourceIntegerMultiplication_restore_step [] left right (true :: restore) output) = some (sourceIntegerMultiplicationConfiguration 4 [] left (true :: right) restore output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_restore_finish @@ -2341,7 +2358,7 @@ theorem sourceIntegerMultiplication_restore_finish [] left right [] output) = some (sourceIntegerMultiplicationConfiguration 2 [] left right [] output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_success_step @@ -2351,7 +2368,7 @@ theorem sourceIntegerMultiplication_success_step [] [] (true :: right) [] output) = some (sourceIntegerMultiplicationConfiguration 5 [] [] right [] output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_success_finish @@ -2361,7 +2378,7 @@ theorem sourceIntegerMultiplication_success_finish [] [] [] [] output) = some (Turing.haltList sourceUnaryIntegerMultiplicationMachine output) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_input_step @@ -2371,7 +2388,7 @@ theorem sourceIntegerMultiplication_failure_input_step (bit :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 6 input left right restore output) := by - cases bit <;> sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_input_finish @@ -2381,7 +2398,7 @@ theorem sourceIntegerMultiplication_failure_input_finish [] left right restore output) = some (sourceIntegerMultiplicationConfiguration 7 [] left right restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_left_step @@ -2391,7 +2408,7 @@ theorem sourceIntegerMultiplication_failure_left_step [] (bit :: left) right restore output) = some (sourceIntegerMultiplicationConfiguration 7 [] left right restore output) := by - cases bit <;> sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_left_finish @@ -2401,7 +2418,7 @@ theorem sourceIntegerMultiplication_failure_left_finish [] [] right restore output) = some (sourceIntegerMultiplicationConfiguration 8 [] [] right restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_right_step @@ -2411,7 +2428,7 @@ theorem sourceIntegerMultiplication_failure_right_step [] [] (bit :: right) restore output) = some (sourceIntegerMultiplicationConfiguration 8 [] [] right restore output) := by - cases bit <;> sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_right_finish @@ -2421,7 +2438,7 @@ theorem sourceIntegerMultiplication_failure_right_finish [] [] [] restore output) = some (sourceIntegerMultiplicationConfiguration 9 [] [] [] restore output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_restore_step @@ -2431,7 +2448,7 @@ theorem sourceIntegerMultiplication_failure_restore_step [] [] [] (bit :: restore) output) = some (sourceIntegerMultiplicationConfiguration 9 [] [] [] restore output) := by - cases bit <;> sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_restore_finish @@ -2441,7 +2458,7 @@ theorem sourceIntegerMultiplication_failure_restore_finish [] [] [] [] output) = some (sourceIntegerMultiplicationConfiguration 10 [] [] [] [] output) := by - sourceIntegerMultiplicationStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_output_step @@ -2451,7 +2468,7 @@ theorem sourceIntegerMultiplication_failure_output_step [] [] [] [] (bit :: output)) = some (sourceIntegerMultiplicationConfiguration 10 [] [] [] [] output) := by - cases bit <;> sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceIntegerMultiplication_failure_finish : @@ -2460,7 +2477,7 @@ theorem sourceIntegerMultiplication_failure_finish : [] [] [] [] []) = some (Turing.haltList sourceUnaryIntegerMultiplicationMachine []) := by - sourceIntegerMultiplicationStepTac + sourceIntegerMultiplicationStepOnly end diff --git a/LeanPool/GapCVP/Part06B.lean b/LeanPool/GapCVP/Part06B.lean index 9efcb6bd8b..a5608539c6 100644 --- a/LeanPool/GapCVP/Part06B.lean +++ b/LeanPool/GapCVP/Part06B.lean @@ -851,6 +851,20 @@ macro "sourceUnaryDivisionStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a source unary division step using the fixed simplification rules. -/ +macro "sourceUnaryDivisionStepOnly" : tactic => + `(tactic| machineStackEquality [ + sourceUnaryDivisionMachine, sourceUnaryDivisionConfiguration, sourceUnaryDivisionControl, + sourceUnaryDivisionPeek, sourceUnaryDivisionPop, sourceUnaryDivisionGoto, + sourceUnaryDivisionDividendStatement, sourceUnaryDivisionModulusStatement, + sourceUnaryDivisionArchiveSuffixStatement, sourceUnaryDivisionRestoreSourceStatement, + sourceUnaryDivisionDispatchStatement, sourceUnaryDivisionMatchStatement, + sourceUnaryDivisionRestoreModulusStatement, sourceUnaryDivisionEmitRemainderStatement, + sourceUnaryDivisionEmitQuotientStatement, sourceUnaryDivisionCleanupModulusStatement, + sourceUnaryDivisionCleanupScratchStatement, sourceUnaryDivisionCleanupDividendStatement, + sourceUnaryDivisionCleanupPartialStatement, Turing.haltList, Turing.FinTM2.step, + Turing.TM2.step, Turing.TM2.stepAux]) + /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_dividend_true (valid : Bool) @@ -863,7 +877,7 @@ theorem sourceUnaryDivision_dividend_true some (sourceUnaryDivisionConfiguration 0 valid input (true :: archive) (true :: dividend) modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_dividend_false @@ -877,7 +891,7 @@ theorem sourceUnaryDivision_dividend_false some (sourceUnaryDivisionConfiguration 1 valid input (false :: archive) dividend modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_dividend_missing @@ -891,7 +905,7 @@ theorem sourceUnaryDivision_dividend_missing some (sourceUnaryDivisionConfiguration 2 false [] archive dividend modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_modulus_true @@ -905,7 +919,7 @@ theorem sourceUnaryDivision_modulus_true some (sourceUnaryDivisionConfiguration 1 valid input (true :: archive) dividend (true :: modulus) modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_modulus_false @@ -919,7 +933,7 @@ theorem sourceUnaryDivision_modulus_false some (sourceUnaryDivisionConfiguration 2 valid input (false :: archive) dividend modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_modulus_missing @@ -933,7 +947,7 @@ theorem sourceUnaryDivision_modulus_missing some (sourceUnaryDivisionConfiguration 2 false [] archive dividend modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_suffix_step @@ -947,7 +961,7 @@ theorem sourceUnaryDivision_suffix_step some (sourceUnaryDivisionConfiguration 2 valid input (bit :: archive) dividend modulus modulusScratch quotient residueStack output) := by - cases bit <;> sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_suffix_finish @@ -961,7 +975,7 @@ theorem sourceUnaryDivision_suffix_finish some (sourceUnaryDivisionConfiguration 3 valid [] archive dividend modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_restoreSource_step @@ -975,7 +989,7 @@ theorem sourceUnaryDivision_restoreSource_step some (sourceUnaryDivisionConfiguration 3 valid [] archive dividend modulus modulusScratch quotient residueStack (bit :: output)) := by - cases bit <;> sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_restoreSource_finish @@ -989,7 +1003,7 @@ theorem sourceUnaryDivision_restoreSource_finish some (sourceUnaryDivisionConfiguration 4 valid [] [] dividend modulus modulusScratch quotient residueStack (false :: output)) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_dispatch_valid @@ -1002,7 +1016,7 @@ theorem sourceUnaryDivision_dispatch_valid some (sourceUnaryDivisionConfiguration 5 true [] [] dividend (true :: modulusTail) modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_dispatch_zero @@ -1014,7 +1028,7 @@ theorem sourceUnaryDivision_dispatch_zero some (sourceUnaryDivisionConfiguration 9 true [] [] dividend [] modulusScratch quotient residueStack (false :: output)) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_dispatch_invalid @@ -1027,7 +1041,7 @@ theorem sourceUnaryDivision_dispatch_invalid some (sourceUnaryDivisionConfiguration 9 false [] [] dividend modulus modulusScratch quotient residueStack (false :: output)) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_match_step @@ -1042,7 +1056,7 @@ theorem sourceUnaryDivision_match_step [] [] dividend modulus (true :: modulusScratch) quotient (true :: residueStack) output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_match_full @@ -1055,7 +1069,7 @@ theorem sourceUnaryDivision_match_full some (sourceUnaryDivisionConfiguration 6 valid [] [] dividend [] modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_match_partial @@ -1068,7 +1082,7 @@ theorem sourceUnaryDivision_match_partial some (sourceUnaryDivisionConfiguration 7 valid [] [] [] (true :: modulus) modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_restoreModulus_step @@ -1081,7 +1095,7 @@ theorem sourceUnaryDivision_restoreModulus_step some (sourceUnaryDivisionConfiguration 6 valid [] [] dividend (true :: modulus) modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_restoreModulus_finish @@ -1092,7 +1106,7 @@ theorem sourceUnaryDivision_restoreModulus_finish [] [] dividend modulus [] quotient [] output) = some (sourceUnaryDivisionConfiguration 5 valid [] [] dividend modulus [] (true :: quotient) [] output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_emitRemainder_step @@ -1105,7 +1119,7 @@ theorem sourceUnaryDivision_emitRemainder_step some (sourceUnaryDivisionConfiguration 7 valid [] [] [] modulus modulusScratch quotient residueStack (true :: output)) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_emitRemainder_finish @@ -1118,7 +1132,7 @@ theorem sourceUnaryDivision_emitRemainder_finish some (sourceUnaryDivisionConfiguration 8 valid [] [] [] modulus modulusScratch quotient [] (false :: output)) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_emitQuotient_step @@ -1131,7 +1145,7 @@ theorem sourceUnaryDivision_emitQuotient_step some (sourceUnaryDivisionConfiguration 8 valid [] [] [] modulus modulusScratch quotient [] (true :: output)) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_emitQuotient_finish @@ -1144,7 +1158,7 @@ theorem sourceUnaryDivision_emitQuotient_finish some (sourceUnaryDivisionConfiguration 9 valid [] [] [] modulus modulusScratch [] [] output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupModulus_step @@ -1157,7 +1171,7 @@ theorem sourceUnaryDivision_cleanupModulus_step some (sourceUnaryDivisionConfiguration 9 valid [] [] dividend modulus modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupModulus_finish @@ -1170,7 +1184,7 @@ theorem sourceUnaryDivision_cleanupModulus_finish some (sourceUnaryDivisionConfiguration 10 valid [] [] dividend [] modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupScratch_step @@ -1183,7 +1197,7 @@ theorem sourceUnaryDivision_cleanupScratch_step some (sourceUnaryDivisionConfiguration 10 valid [] [] dividend [] modulusScratch quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupScratch_finish @@ -1194,7 +1208,7 @@ theorem sourceUnaryDivision_cleanupScratch_finish [] [] dividend [] [] quotient residueStack output) = some (sourceUnaryDivisionConfiguration 11 valid [] [] dividend [] [] quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupDividend_step @@ -1205,7 +1219,7 @@ theorem sourceUnaryDivision_cleanupDividend_step [] [] (true :: dividend) [] [] quotient residueStack output) = some (sourceUnaryDivisionConfiguration 11 valid [] [] dividend [] [] quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupDividend_finish @@ -1216,7 +1230,7 @@ theorem sourceUnaryDivision_cleanupDividend_finish [] [] [] [] [] quotient residueStack output) = some (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] quotient residueStack output) := by - sourceUnaryDivisionStepTac + rfl /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupPartial_step @@ -1227,7 +1241,7 @@ theorem sourceUnaryDivision_cleanupPartial_step [] [] [] [] [] quotient (true :: residueStack) output) = some (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] quotient residueStack output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly /-- Internal support shared across GapCVP continuation modules. -/ theorem sourceUnaryDivision_cleanupPartial_finish @@ -1236,7 +1250,7 @@ theorem sourceUnaryDivision_cleanupPartial_finish (sourceUnaryDivisionConfiguration 12 valid [] [] [] [] [] [] [] output) = some (Turing.haltList sourceUnaryDivisionMachine output) := by - sourceUnaryDivisionStepTac + sourceUnaryDivisionStepOnly end diff --git a/LeanPool/GapCVP/Part06D.lean b/LeanPool/GapCVP/Part06D.lean index 49720f1e39..24d1545f04 100644 --- a/LeanPool/GapCVP/Part06D.lean +++ b/LeanPool/GapCVP/Part06D.lean @@ -2330,7 +2330,7 @@ private theorem fiveFamilySourceCellPositiveLiteralList_nodup intro first second hequal have hsymbol := congrArg (fun literal : SignedLiteral T S => literal.1.2.2) hequal - simpa only [positive] using hsymbol + exact hsymbol private theorem fiveFamilySourceCellPositiveLiteralList_pairwise {T S : ℕ} (time : Time T) (position : Position T) : @@ -2391,7 +2391,7 @@ private theorem fiveFamilySourceAcceptancePositiveLiteralList_nodup intro first second hequal have hposition := congrArg (fun literal : SignedLiteral T S => literal.1.2.1) hequal - simpa only [positive] using hposition + exact hposition private theorem fiveFamilySourceAcceptancePositiveLiteralList_pairwise {T S : ℕ} (accept : Symbol S) : diff --git a/LeanPool/GapCVP/Part07A.lean b/LeanPool/GapCVP/Part07A.lean index 109dde6b15..18ae16cb61 100644 --- a/LeanPool/GapCVP/Part07A.lean +++ b/LeanPool/GapCVP/Part07A.lean @@ -1849,10 +1849,10 @@ theorem fiveFamilyPackedInitialDecodedCell_valid rw [← hcenterLength, List.drop_append_length] have htake' : (center ++ head).take (6 * blockSize machine.tm) = center := by - simpa only [block] using htake + exact htake have hdrop' : (center ++ head).drop (6 * blockSize machine.tm) = head := by - simpa only [block] using hdrop + exact hdrop change fiveFamilyPackedInitialDecodedCell machine (center ++ head) = initialPhaseCell bound machine original position unfold fiveFamilyPackedInitialDecodedCell diff --git a/LeanPool/GapCVP/Part07C.lean b/LeanPool/GapCVP/Part07C.lean index efb9c40f06..d7b864182f 100644 --- a/LeanPool/GapCVP/Part07C.lean +++ b/LeanPool/GapCVP/Part07C.lean @@ -318,7 +318,7 @@ private theorem flatAnnotatedCountedSourceFieldTail_length_le input.length have hprevious : (((firstFieldSuffix^[offset]) input)).length ≤ input.length := by - simpa only [flatAnnotatedSourceFieldTail] using ih + exact ih omega private theorem countedFieldAt_length_le @@ -1908,7 +1908,7 @@ private theorem flatAnnotatedSquareResolutionStep_iterate_pairs rw [List.length_cons, Function.iterate_succ_apply] simp only [List.flatMap_cons, List.append_assoc] rw [flatAnnotatedSquareResolutionStep_state] - simpa only [List.foldl_cons] using ih (resolveFlatSourceOrder major pair.1 pair.2) + exact ih (resolveFlatSourceOrder major pair.1 pair.2) private theorem flatAnnotatedSquareResolutionStep_outer (major archive suffix : List Bool) : diff --git a/LeanPool/GapCVP/Part07D.lean b/LeanPool/GapCVP/Part07D.lean index 80128c77fe..95128767e6 100644 --- a/LeanPool/GapCVP/Part07D.lean +++ b/LeanPool/GapCVP/Part07D.lean @@ -1119,12 +1119,10 @@ private theorem flatAnnotatedCompleteNonemptyMatchedDecomposition nextFirst, nextSecond, firstRemaining, secondRemaining, ?_, ?_, ?_, hshort⟩ - · simpa only [List.map_cons, List.cons_append] - using congrArg + · exact congrArg (fun source : List ℕ => firstHead :: source) hfirstTail - · simpa only [List.map_cons, List.cons_append] - using congrArg + · exact congrArg (fun source : List ℕ => secondHead :: source) hsecondTail · simp only [List.length_cons] at hcount ⊢ diff --git a/LeanPool/GapCVP/Part08A.lean b/LeanPool/GapCVP/Part08A.lean index c290f3bfbf..62250aab1b 100644 --- a/LeanPool/GapCVP/Part08A.lean +++ b/LeanPool/GapCVP/Part08A.lean @@ -464,7 +464,7 @@ private theorem fiveFamilyForbiddenExactWindowDescriptorPayloadWord_valid (fun atom => flatSignedLiteralDescriptor (sourceLiteral (negative atom))) (fun atom => by - simpa only [sourceLiteral, negative] using + exact tableauSourceSignedLiteralDescriptorWord_variable atom false) rw [hphysical] simp only [flatSourceClauseDescriptorPayload, @@ -497,7 +497,7 @@ private theorem fiveFamilyForbiddenExactWindowDuplicatedPayloadWord_valid (fun atom => flatDuplicatedUnaryField (Encodable.encode (negative atom))) (fun atom => by - simpa only [negative] using + exact duplicatedUnarySignedLiteralCodeWord_sourceVariable atom false) rw [hphysical] simp only [flatSourceClauseDuplicatedCodePayload, diff --git a/LeanPool/GapCVP/Part08D.lean b/LeanPool/GapCVP/Part08D.lean index 0d6da721f9..76b2842245 100644 --- a/LeanPool/GapCVP/Part08D.lean +++ b/LeanPool/GapCVP/Part08D.lean @@ -401,8 +401,7 @@ private noncomputable def flatIndexedSourceORPaddingDescriptorComputable flatSignedLiteralDescriptor (if negated then negate literal else literal) := by rcases literal with ⟨index, sign⟩ - cases negated <;> cases sign <;> - simp [flatIndexedGadgetSourceDescriptorWord, + cases negated <;> simp [flatIndexedGadgetSourceDescriptorWord, flatIndexedGadgetSourcePayloadWord, flatIndexedGadgetNegateLeadingBitWord, flatAnnotatedSourceFieldAt, flatAnnotatedSourceFieldTail, @@ -1132,8 +1131,7 @@ private theorem flatIndexedPairedAccumulatorDescriptorWord_length_le false :: (List.replicate second true ++ [false])) = flatSignedLiteralDescriptor (accumulatorVariable first second, sign) := by - simpa only [unarySourcePairWord] - using (pairedAccumulatorSignedLiteralDescriptorWord_pair first second sign) + exact (pairedAccumulatorSignedLiteralDescriptorWord_pair first second sign) rw [pair] simp only [List.length_append, List.length_replicate, List.length_cons, List.length_nil] @@ -1786,10 +1784,7 @@ private theorem flatAnnotatedIndexedORGadgetStartState_valid (flatThreeClauseLiterals (paddedUnary (accumulatorLiteral clauseIndex 0 true))) := by - simpa only [orGadgetIdleState, orGadgetPhysicalState, - CNFFiveFamilySourceIndexedORGadgetFoldCoreTM.flatAnnotatedIndexedORGadgetState, - List.append_assoc, - CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatAnnotatedIndexedORGadgetState] using + exact flatIndexedSourceORPaddingDescriptorWord_valid_initial clauseIndex true (flatAnnotatedBundledClauseStream (clause :: remaining)) [] (flatSignedLiteralDescriptorStream (flatThreeClauseLiterals emitted)) (List.replicate @@ -1846,11 +1841,7 @@ private theorem flatAnnotatedIndexedORGadgetGateState_valid (orGate (sourceLiteral literal) (accumulatorLiteral clauseIndex (prefixIndex + 1) true) (accumulatorLiteral clauseIndex prefixIndex true))) := by - simpa only [orGadgetActiveState, orGadgetPhysicalState, - CNFFiveFamilySourceIndexedORGadgetFoldCoreTM.flatAnnotatedIndexedORGadgetState, - List.append_assoc, - flatSignedLiteralDescriptorStream, List.map_cons, List.flatMap_cons, - CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatAnnotatedIndexedORGadgetState] using + exact flatIndexedSourceORGadgetDescriptorWord_valid clauseIndex prefixIndex (sourceLiteral literal) (flatAnnotatedBundledClauseStream pending) (flatSignedLiteralDescriptorStream @@ -1919,11 +1910,7 @@ private theorem flatAnnotatedIndexedORGadgetFinishState_valid (flatThreeClauseLiterals (paddedUnary (accumulatorLiteral clauseIndex prefixIndex false))) := by - simpa only [orGadgetActiveState, orGadgetPhysicalState, - CNFFiveFamilySourceIndexedORGadgetFoldCoreTM.flatAnnotatedIndexedORGadgetState, - List.append_assoc, - flatSignedLiteralDescriptorStream, List.map_nil, List.flatMap_nil, - CNFFiveFamilySourceIndexedORGadgetRecordWorkerTM.flatAnnotatedIndexedORGadgetState] using + exact flatIndexedSourceORPaddingDescriptorWord_valid clauseIndex prefixIndex false (flatAnnotatedBundledClauseStream pending) [] (flatSignedLiteralDescriptorStream (flatThreeClauseLiterals emitted)) (List.replicate @@ -4353,7 +4340,7 @@ private theorem hankel_eq_vandermonde_transpose_mul {R : Type*} [CommRing R] (Matrix.of fun i j : Fin n => ∑ k : Fin n, v k ^ (i.val + j.val)) = (Matrix.vandermonde v)ᵀ * Matrix.vandermonde v := by ext i j - simpa only [of_apply] using (Matrix.vandermonde_transpose_mul_vandermonde v i j).symm + exact (Matrix.vandermonde_transpose_mul_vandermonde v i j).symm theorem hankel_det_eq_vandermonde_det_sq {R : Type*} [CommRing R] {n : ℕ} (v : Fin n → R) : @@ -4536,7 +4523,7 @@ private theorem exists_mem_of_mem_paritySupport a ∈ s ∧ a ∉ paritySupport supports ∨ a ∈ paritySupport supports ∧ a ∉ s := by apply Finset.mem_symmDiff.mp - simpa only [paritySupport] using ha + exact ha rcases hcases with ⟨has, _⟩ | ⟨haparity, _⟩ · exact ⟨s, by simp only [List.mem_cons, true_or], has⟩ · obtain ⟨t, ht, hat⟩ := ih haparity diff --git a/LeanPool/GapCVP/Part09.lean b/LeanPool/GapCVP/Part09.lean index 94abbe062e..c23021a2d7 100644 --- a/LeanPool/GapCVP/Part09.lean +++ b/LeanPool/GapCVP/Part09.lean @@ -14,7 +14,6 @@ public import Mathlib.RingTheory.Valuation.Basic import Mathlib.Algebra.Order.Floor.Semifield import Mathlib.Algebra.Order.Star.Int import Mathlib.FieldTheory.RatFunc.AsPolynomial -import Mathlib.RingTheory.Flat.TorsionFree import Mathlib.RingTheory.Henselian import Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities @@ -468,7 +467,7 @@ private theorem orderedInterpolationNode_injective {p D : ℕ} Fin.castLE (Nat.succ_le_of_lt hdegree) second := hpoints heq apply Fin.ext - simpa only [Nat.succ_eq_add_one, Fin.val_castLE] using congrArg (fun index : Fin p => index.val) + exact congrArg (fun index : Fin p => index.val) hcast /-- GapCVP reduction support. -/ @@ -1023,7 +1022,7 @@ private theorem rootSupportPolynomial_monic {h : ℕ} (roots : Fin h → K) : (rootSupportPolynomial roots).Monic := by classical - simpa only [rootSupportPolynomial] using Polynomial.monic_prod_X_sub_C roots (Finset.univ : + exact Polynomial.monic_prod_X_sub_C roots (Finset.univ : Finset (Fin h)) private theorem rootSupportPolynomial_natDegree @@ -1247,8 +1246,7 @@ private theorem genericHankelDenominator_eval (genericHankelDenominator h moments).eval point = ((polynomialHankel moments h).map (Polynomial.evalRingHom point)).det := by - simpa only [genericHankelDenominator, leadingHankelDet, coe_evalRingHom, - RingHom.mapMatrix_apply] using + exact ((Polynomial.evalRingHom point).map_det (polynomialHankel moments h)) _ = (powerSumHankel roots).det := by rw [polynomialHankel_specializes moments point roots hmoments] @@ -1556,7 +1554,7 @@ private theorem separable_ratFunc_map_of_separable_specialization let fiber : K[X] := polynomial.map evaluation let generic : (RatFunc K)[X] := polynomial.map embedding have hinjective : Function.Injective embedding := by - exact FaithfulSMul.algebraMap_injective K[X] (RatFunc K) + exact RatFunc.algebraMap_injective K have hfiberseparable : fiber.Separable := by simpa only using hspecial have hfiberdegree : fiber.natDegree = polynomial.natDegree := by @@ -1782,13 +1780,16 @@ private theorem clearedGenericMomentSupportPolynomial_map_ratFunc (algebraMap K[X] (RatFunc K) (genericHankelDenominator h moments)) * genericMomentSupportPolynomial h moments := by + let : FaithfulSMul K[X] (RatFunc K) := + (faithfulSMul_iff_algebraMap_injective K[X] (RatFunc K)).mpr + (RatFunc.algebraMap_injective K) classical have hdenominator' : algebraMap K[X] (RatFunc K) (genericHankelDenominator h moments) ≠ 0 := by intro hzero apply hdenominator - apply FaithfulSMul.algebraMap_injective K[X] (RatFunc K) + apply RatFunc.algebraMap_injective K simpa only [map_zero, FaithfulSMul.algebraMap_eq_zero_iff] using hzero unfold clearedGenericMomentSupportPolynomial genericMomentSupportPolynomial @@ -1937,8 +1938,7 @@ private theorem genericHankelDenominator_eval_eq_zero_of_smaller_fiber (genericHankelDenominator rank moments).eval point = ((polynomialHankel moments rank).map (Polynomial.evalRingHom point)).det := by - simpa only [genericHankelDenominator, leadingHankelDet, coe_evalRingHom, - RingHom.mapMatrix_apply] using + exact (Polynomial.evalRingHom point).map_det (polynomialHankel moments rank) _ = (fiberPowerSumHankel rank roots).det := by rw [polynomialHankel_specializes_fiberPowerSumHankel @@ -2040,9 +2040,12 @@ private theorem genericHankelDenominator_ratFunc_ne_zero_of_polynomial (hdenominator : genericHankelDenominator h moments ≠ 0) : algebraMap K[X] (RatFunc K) (genericHankelDenominator h moments) ≠ 0 := by + let : FaithfulSMul K[X] (RatFunc K) := + (faithfulSMul_iff_algebraMap_injective K[X] (RatFunc K)).mpr + (RatFunc.algebraMap_injective K) intro hzero apply hdenominator - apply FaithfulSMul.algebraMap_injective K[X] (RatFunc K) + apply RatFunc.algebraMap_injective K simpa only [map_zero, FaithfulSMul.algebraMap_eq_zero_iff] using hzero private def universalElementaryPowerSum @@ -2180,7 +2183,7 @@ private theorem clearedMvPolynomialEvaluation_map (∏ i ∈ exponent.support, map denominator ^ exponent i) = map denominator ^ exponent.sum (fun _ power => power) := by - simpa only [Finsupp.sum] using + exact Finset.prod_pow_eq_pow_sum exponent.support (fun i => exponent i) (map denominator) simp only [RingHom.coe_comp, Function.comp_apply] simp_rw [div_pow] @@ -2254,7 +2257,7 @@ private theorem clearedGenericRootPowerSum_map_ratFunc (Polynomial.C : K →+* K[X]) = algebraMap K (RatFunc K) := by symm - simpa only [Polynomial.algebraMap_eq] using + exact IsScalarTower.algebraMap_eq K K[X] (RatFunc K) have hvariables : (fun i : Fin h => @@ -2450,7 +2453,7 @@ private theorem genericRootPowerSum_map_eq_rootMoment (supportElementaryCoefficients (genericHankelCoefficient h moments) i)) (universalElementaryPowerSum K h j) := by - simpa only [IsScalarTower.toAlgHom_apply] using + exact MvPolynomial.comp_aeval_apply (supportElementaryCoefficients (genericHankelCoefficient h moments)) @@ -4834,7 +4837,7 @@ private theorem functionFieldExtendedValuation_monic_root_separation apply hsum have heval := hroot rw [Polynomial.eval₂_eq_sum, Polynomial.sum_def] at heval - simpa only using heval + exact heval private def normalizedAffineRootPolynomial {k : Type*} [Field k] @@ -5353,8 +5356,7 @@ theorem BinaryAffineSystem.effectiveGaussian_solves_iff (H : BinaryAffineSystem) (z : Fin H.dimension → ℤ) : H.effectiveGaussianState.system.Satisfies (binaryResidue z) ↔ H.Solves z := by - simpa only [EffectiveBinaryGaussian.System.Satisfies, - effectiveGaussianState, effectiveGaussianSystem, Solves] using + exact EffectiveBinaryGaussian.eliminate_satisfies_iff H.effectiveGaussianSystem (binaryResidue z) /-- GapCVP reduction support. -/ @@ -5774,6 +5776,14 @@ macro "preservingXorStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a preserving XOR step using the fixed simplification rules. -/ +macro "preservingXorStepOnly" : tactic => + `(tactic| machineStackEquality [ + preservingXorMachine, preservingXorConfiguration, preservingXorPeek, preservingXorGoto, + preservingXorFirstStatement, preservingXorSecondStatement, preservingXorScanStatement, + preservingXorRestoreStatement, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + private theorem preservingXor_first_step (first : Bool) (remaining archive output : List Bool) : preservingXorMachine.step @@ -5781,14 +5791,14 @@ private theorem preservingXor_first_step (first :: remaining) archive output) = some (preservingXorConfiguration 1 (some first) remaining archive output) := by - cases first <;> preservingXorStepTac + cases first <;> preservingXorStepOnly private theorem preservingXor_first_missing (archive output : List Bool) : preservingXorMachine.step (preservingXorConfiguration 0 none [] archive output) = some (preservingXorConfiguration 2 none [] archive output) := by - preservingXorStepTac + rfl private theorem preservingXor_second_step (first second : Bool) (remaining archive output : List Bool) : @@ -5797,14 +5807,18 @@ private theorem preservingXor_second_step (second :: remaining) archive output) = some (preservingXorConfiguration 2 none remaining (Bool.xor first second :: archive) output) := by - cases first <;> cases second <;> preservingXorStepTac + cases first <;> cases second <;> reduceMachineConfiguration + [preservingXorConfiguration] + (preservingXorStepTac) private theorem preservingXor_second_missing (first : Bool) (archive output : List Bool) : preservingXorMachine.step (preservingXorConfiguration 1 (some first) [] archive output) = some (preservingXorConfiguration 2 none [] archive output) := by - cases first <;> preservingXorStepTac + cases first <;> reduceMachineConfiguration + [preservingXorConfiguration] + (preservingXorStepTac) private theorem preservingXor_scan_step (bit : Bool) (remaining archive output : List Bool) : @@ -5813,14 +5827,14 @@ private theorem preservingXor_scan_step (bit :: remaining) archive output) = some (preservingXorConfiguration 2 none remaining (bit :: archive) output) := by - cases bit <;> preservingXorStepTac + preservingXorStepOnly private theorem preservingXor_scan_finish (archive output : List Bool) : preservingXorMachine.step (preservingXorConfiguration 2 none [] archive output) = some (preservingXorConfiguration 3 none [] archive output) := by - preservingXorStepTac + rfl private theorem preservingXor_restore_step (bit : Bool) (archive output : List Bool) : @@ -5829,14 +5843,14 @@ private theorem preservingXor_restore_step (bit :: archive) output) = some (preservingXorConfiguration 3 none [] archive (bit :: output)) := by - cases bit <;> preservingXorStepTac + preservingXorStepOnly private theorem preservingXor_restore_finish (output : List Bool) : preservingXorMachine.step (preservingXorConfiguration 3 none [] [] output) = some (Turing.haltList preservingXorMachine output) := by - preservingXorStepTac + preservingXorStepOnly private def preservingXor_scanTrace (input archive output : List Bool) : @@ -6367,6 +6381,14 @@ macro "binaryGaussianXorStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a binary Gaussian XOR step using the fixed simplification rules. -/ +macro "binaryGaussianXorStepOnly" : tactic => + `(tactic| machineStackEquality [ + binaryGaussianXorMachine, binaryGaussianXorConfiguration, binaryGaussianXorPeek, + binaryGaussianXorGoto, binaryGaussianXorFirstStatement, binaryGaussianXorSecondStatement, + binaryGaussianXorDrainStatement, Turing.haltList, Turing.FinTM2.step, Turing.TM2.step, + Turing.TM2.stepAux]) + private theorem binaryGaussianXor_first_step (first : Bool) (remaining output : List Bool) : binaryGaussianXorMachine.step @@ -6374,14 +6396,14 @@ private theorem binaryGaussianXor_first_step (first :: remaining) output) = some (binaryGaussianXorConfiguration 1 (some first) remaining output) := by - cases first <;> binaryGaussianXorStepTac + cases first <;> binaryGaussianXorStepOnly private theorem binaryGaussianXor_first_missing (output : List Bool) : binaryGaussianXorMachine.step (binaryGaussianXorConfiguration 0 none [] output) = some (binaryGaussianXorConfiguration 2 none [] output) := by - binaryGaussianXorStepTac + rfl private theorem binaryGaussianXor_second_step (first second : Bool) (remaining output : List Bool) : @@ -6390,14 +6412,18 @@ private theorem binaryGaussianXor_second_step (second :: remaining) output) = some (binaryGaussianXorConfiguration 2 none remaining (Bool.xor first second :: output)) := by - cases first <;> cases second <;> binaryGaussianXorStepTac + cases first <;> cases second <;> reduceMachineConfiguration + [binaryGaussianXorConfiguration] + (binaryGaussianXorStepTac) private theorem binaryGaussianXor_second_missing (first : Bool) (output : List Bool) : binaryGaussianXorMachine.step (binaryGaussianXorConfiguration 1 (some first) [] output) = some (binaryGaussianXorConfiguration 2 none [] output) := by - cases first <;> binaryGaussianXorStepTac + cases first <;> reduceMachineConfiguration + [binaryGaussianXorConfiguration] + (binaryGaussianXorStepTac) private theorem binaryGaussianXor_drain_step (bit : Bool) (remaining output : List Bool) : @@ -6406,13 +6432,13 @@ private theorem binaryGaussianXor_drain_step (bit :: remaining) output) = some (binaryGaussianXorConfiguration 2 none remaining output) := by - cases bit <;> binaryGaussianXorStepTac + binaryGaussianXorStepOnly private theorem binaryGaussianXor_drain_finish (output : List Bool) : binaryGaussianXorMachine.step (binaryGaussianXorConfiguration 2 none [] output) = some (Turing.haltList binaryGaussianXorMachine output) := by - binaryGaussianXorStepTac + binaryGaussianXorStepOnly private def binaryGaussianXor_drainTrace (input output : List Bool) : @@ -8431,8 +8457,13 @@ private theorem sourceFormulaShiftedCommonRoot_separation encodingLength F localVar.val)))) ^ sourceFormulaGenericRank encodingLength F z hz (.inr ⟨clause, tuple⟩) := by - simpa only [sourceFormulaNormalizedAffineRootPolynomial_natDegree] using - functionFieldExtendedValuation_monic_root_separation + have degree : + (sourceFormulaNormalizedAffineRootPolynomial + encodingLength F z hz clause tuple localVar).natDegree = + sourceFormulaGenericRank encodingLength F z hz (.inr ⟨clause, tuple⟩) := by + simp only [sourceFormulaNormalizedAffineRootPolynomial_natDegree] + apply LE.le.trans_eq + (functionFieldExtendedValuation_monic_root_separation (sourceFormulaVariablePlace encodingLength F localVar.val) (sourceFormulaNormalizedAffineRootPolynomial encodingLength F z hz clause tuple localVar) @@ -8440,7 +8471,8 @@ private theorem sourceFormulaShiftedCommonRoot_separation encodingLength F z hz clause tuple localVar) _ (sourceFormulaNormalizedAffineRootPolynomial_eval₂_eq_zero encodingLength F z hz hshort clause tuple localVar index) - hlarge + hlarge) + exact congrArg (fun exponent : ℕ => _ ^ exponent) degree theorem sourceFormulaShiftedCommonRoot_highPower_separation (encodingLength : ℕ) (F : Formula) diff --git a/LeanPool/GapCVP/Part10A.lean b/LeanPool/GapCVP/Part10A.lean index 00bbf9df72..c0d50a983d 100644 --- a/LeanPool/GapCVP/Part10A.lean +++ b/LeanPool/GapCVP/Part10A.lean @@ -747,6 +747,15 @@ theorem adaptGapCVPInstance_gapNO400_iff_metricNo (GapCVP.Core.effectiveConstructionAInstance H hdimension radius hradius) +/-- Read the constructed basis without unfolding Gaussian elimination. -/ +theorem effectiveGapCVPInstance_basis + (system : GapCVP.Core.BinaryAffineSystem) + (positiveDimension : 0 < system.dimension) + (radius : ℚ) (radiusPositive : 0 < radius) + (row column : Fin system.dimension) : + (effectiveGapCVPInstance system positiveDimension radius radiusPositive).basis row column = + system.effectiveSquareBasisMatrix row column := rfl + theorem effectiveGapCVPInstance_wellFormed (H : GapCVP.Core.BinaryAffineSystem) (hdimension : 0 < H.dimension) @@ -1915,7 +1924,7 @@ private theorem runColumns_pivots_pairwise (runColumns columns state).pivots.Pairwise (fun p q => p.1 ≠ q.1) := by induction columns generalizing scanned state with - | nil => simpa only [ne_eq, runColumns, List.foldl_nil] using hunique + | nil => exact hunique | cons column rest ih => change (runColumns rest (columnStep state column)).pivots.Pairwise @@ -1927,7 +1936,7 @@ private theorem runColumns_pivots_pairwise private theorem eliminate_pivots_pairwise {m n : ℕ} (system : System m n) : (eliminate system).pivots.Pairwise (fun p q => p.1 ≠ q.1) := by - simpa only [ne_eq, eliminate] using + exact (runColumns_pivots_pairwise (List.finRange n) [] (initialState system) (initialState_prefixNormal system) (by simp [initialState])) @@ -2321,7 +2330,7 @@ theorem BinaryAffineSystem.effectiveGaussian_kernel_iff_graph_of_normal if H.effectivePivotRowOption column = none then H.effectiveGaussianState.system.check pivotRow column * bits column - else 0)).mp (by simpa only [Pi.zero_apply] using hrow) + else 0)).mp (by exact hrow) · intro hgraph funext row by_cases hrow : row.val < H.effectiveGaussianState.nextPivot diff --git a/LeanPool/GapCVP/Part10B.lean b/LeanPool/GapCVP/Part10B.lean index 6f531a5b88..7e9386c9b9 100644 --- a/LeanPool/GapCVP/Part10B.lean +++ b/LeanPool/GapCVP/Part10B.lean @@ -2100,51 +2100,58 @@ macro "binaryGaussianPivotStepTac" : tactic => (first | rfl | simp [Function.update]) } <;> try rfl))) +/-- Prove a binary Gaussian pivot step using the fixed simplification rules. -/ +macro "binaryGaussianPivotStepOnly" : tactic => + `(tactic| machineStackEquality [ + binaryGaussianPivotMachine, pivotConfiguration, pivotPeek, pivotGoto, pivotScanStatement, + pivotSuccessDrainStatement, pivotFailureStatement, Turing.haltList, Turing.FinTM2.step, + Turing.TM2.step, Turing.TM2.stepAux]) + private theorem pivot_scan_false (input output : List Bool) : binaryGaussianPivotMachine.step (pivotConfiguration 0 (false :: input) output) = some (pivotConfiguration 0 input (true :: output)) := by - binaryGaussianPivotStepTac + binaryGaussianPivotStepOnly private theorem pivot_scan_true (input output : List Bool) : binaryGaussianPivotMachine.step (pivotConfiguration 0 (true :: input) output) = some (pivotConfiguration 1 input (true :: output)) := by - binaryGaussianPivotStepTac + binaryGaussianPivotStepOnly private theorem pivot_scan_missing (output : List Bool) : binaryGaussianPivotMachine.step (pivotConfiguration 0 [] output) = some (pivotConfiguration 2 [] output) := by - binaryGaussianPivotStepTac + rfl private theorem pivot_success_drain_step (bit : Bool) (input output : List Bool) : binaryGaussianPivotMachine.step (pivotConfiguration 1 (bit :: input) output) = some (pivotConfiguration 1 input output) := by - cases bit <;> binaryGaussianPivotStepTac + binaryGaussianPivotStepOnly private theorem pivot_success_finish (output : List Bool) : binaryGaussianPivotMachine.step (pivotConfiguration 1 [] output) = some (Turing.haltList binaryGaussianPivotMachine output) := by - binaryGaussianPivotStepTac + binaryGaussianPivotStepOnly private theorem pivot_failure_drain_step (bit : Bool) (output : List Bool) : binaryGaussianPivotMachine.step (pivotConfiguration 2 [] (bit :: output)) = some (pivotConfiguration 2 [] output) := by - cases bit <;> binaryGaussianPivotStepTac + binaryGaussianPivotStepOnly private theorem pivot_failure_finish : binaryGaussianPivotMachine.step (pivotConfiguration 2 [] []) = some (Turing.haltList binaryGaussianPivotMachine [false]) := by - binaryGaussianPivotStepTac + binaryGaussianPivotStepOnly private def pivot_successDrainTrace (input output : List Bool) : @@ -3247,7 +3254,7 @@ private theorem effectiveGaussianPivotCandidates_findIdxOption state.system.check row column = (1 : ZMod 2))) with | none => rfl | some row => - simpa only [Option.bind_some, Option.map_some] using finRange_idxOfOption_eq_some row + exact finRange_idxOfOption_eq_some row theorem binaryGaussianPivotWord_effective {m n : ℕ} (state : State m n) (column : Fin n) : @@ -3789,11 +3796,11 @@ private theorem sourcePhysicalLagrangeProduct_iterate_length_le have hanchor' : (sourcePhysicalLagrangeProductAnchor current).length ≤ state.length := by - simpa only using hcurrentAnchor.symm ▸ hanchor + exact hcurrentAnchor.symm ▸ hanchor have hacc' : (sourcePhysicalLagrangeProductAccumulator current).length ≤ state.length := by - simpa only using hcurrentAccumulator.symm ▸ hacc + exact hcurrentAccumulator.symm ▸ hacc omega private def sourcePhysicalLagrangeProductStatePolynomial : Polynomial ℕ := @@ -3931,7 +3938,7 @@ private theorem sourcePhysicalLagrangeProduct_iterate_valid (GapCVP.Core.EffectiveBinaryField.multiplyMod lower initial factor) factors source) = _ - simpa only [List.foldl_cons] using ih (GapCVP.Core.EffectiveBinaryField.multiplyMod lower + exact ih (GapCVP.Core.EffectiveBinaryField.multiplyMod lower initial factor) /-- GapCVP reduction support. -/ diff --git a/LeanPool/GapCVP/Part11C.lean b/LeanPool/GapCVP/Part11C.lean index 7e46d33ceb..829dadb18e 100644 --- a/LeanPool/GapCVP/Part11C.lean +++ b/LeanPool/GapCVP/Part11C.lean @@ -1052,7 +1052,7 @@ private theorem factor400BinarySourceModularPhysicalCellOutput_query simp only [Bool.true_and, ↓reduceIte] rw [factor400BinarySourceModularShiftXor_coefficient lower leading.val (xorAt current leading true) - (by simpa only [leading] using hposition) + (by exact hposition) (⟨rank, hrank⟩ : Fin (2 * degree))] by_cases hrankLeading : rank = leading.val · have hindex : @@ -1064,7 +1064,7 @@ private theorem factor400BinarySourceModularPhysicalCellOutput_query have hdifference : leading.val - (leading.val - degree) = degree := by have hbound : degree ≤ leading.val := by - simpa only [leading] using hposition.1 + exact hposition.1 omega have hdrop : (finiteWordBits lower).drop @@ -1364,8 +1364,7 @@ private theorem factor400BinarySourceModularReduction_iterate_valid (finiteWordBits (reducePrefix lower stage product)) source := by induction stage with | zero => - simpa only [Function.iterate_zero, id_eq, - reducePrefix, List.range_zero, List.foldl_nil] using + exact factor400BinarySourceModularReductionInitialState_degreeState (finiteWordBits lower) (finiteWordBits product) source | succ stage ih => @@ -3540,7 +3539,7 @@ theorem finitePExponent_cast (p : ℚ) (hp : 1 ≤ p) : have habs : (p.num.natAbs : ℤ) = p.num := Int.natAbs_of_nonneg hnum congr 1 - simpa only [Int.cast_natCast] using + exact congrArg (fun value : ℤ => (value : ℝ)) habs.symm theorem four_mul_le_finitePRadiusScale (p : ℚ) : @@ -4973,9 +4972,7 @@ private theorem paperSourceLiteralEraseDups_nodup theorem paperNormalizedClause_length_le_three (clause : ThreeClause) : (paperSourceNormalizedClause clause).length ≤ 3 := by - simpa only [paperSourceNormalizedClause, paperSourceClauseLiterals, Fin.isValue, - List.length_cons, - List.length_nil, zero_add, Nat.reduceAdd] using + exact paperSourceLiteralEraseDups_length_le (paperSourceClauseLiterals clause) theorem paperSourceNormalizedClause_ne_nil diff --git a/LeanPool/GapCVP/Part12C.lean b/LeanPool/GapCVP/Part12C.lean index 39eca49d10..01bfe6e4f2 100644 --- a/LeanPool/GapCVP/Part12C.lean +++ b/LeanPool/GapCVP/Part12C.lean @@ -2669,7 +2669,7 @@ private theorem paperVariableArityCanonicalBinaryMatrixCheckFold_valid paperVariableArityCanonicalBinaryMatrixCheckFoldPreparation_valid shape formula] unfold sourcePhysicalWordPackedQueryPreparation - simpa only [fourFamilyOriginalMarkerStream] using + exact boundedRecordFoldOutput_sourceFourFamilyOriginalMarkerQueries (paperCanonicalBinaryMatrixCheckMarker worker) (paperCanonicalBinaryMatrixCheckQueries shape formula) (lengthPrefixedWord (encodeThreeCNF @@ -2690,7 +2690,7 @@ private theorem paperVariableArityCanonicalBinaryMatrixRhsFold_valid paperVariableArityCanonicalBinaryMatrixRhsFoldPreparation_valid shape formula] unfold sourcePhysicalWordPackedQueryPreparation - simpa only [fourFamilyOriginalMarkerStream] using + exact boundedRecordFoldOutput_sourceFourFamilyOriginalMarkerQueries (paperCanonicalBinaryMatrixRhsMarker worker) (paperCanonicalBinaryMatrixRhsQueries shape formula) (lengthPrefixedWord (encodeThreeCNF @@ -2903,7 +2903,7 @@ private theorem paperVariableArityCanonicalBinaryMatrixComputedRhsBits_valid formula).rightHandSide row = (1 : ZMod 2))]) := by apply List.flatMap_congr intro row _ - simpa only [column] using paperVariableArityCanonicalBinaryMatrixRhsMarker_valid worker + exact paperVariableArityCanonicalBinaryMatrixRhsMarker_valid worker formula row column _ = (List.finRange diff --git a/LeanPool/GapCVP/Part13.lean b/LeanPool/GapCVP/Part13.lean index 1fa62479f8..2ed796c6d0 100644 --- a/LeanPool/GapCVP/Part13.lean +++ b/LeanPool/GapCVP/Part13.lean @@ -1498,7 +1498,7 @@ private theorem gaussianPhysicalRunColumns_nextPivot_le (hnext : state.nextPivot ≤ m) : (runColumns columns state).nextPivot ≤ m := by induction columns generalizing state with - | nil => simpa only [runColumns, List.foldl_nil] using hnext + | nil => exact hnext | cons column remaining ih => change (runColumns remaining (columnStep state column)).nextPivot ≤ m @@ -1802,7 +1802,7 @@ private theorem gaussianPhysicalColumnIterationOutput_effective effectiveGaussianPackedStateWord (eliminate system) source := by have hnext := gaussianPhysicalInitialState_nextPivot_le system - simpa only [eliminate] using + exact gaussianPhysicalColumnIterationOutput_state_effective (initialState system) source hrows hnext @@ -1844,13 +1844,13 @@ private theorem paperVariableArityPhysicalWordBinarySystem_rowCount_pos (sourceSizeParameter_ge_one_hundred encodingLength normalized) have hgrid : 0 < Fintype.card (ExplicitGridPoint encodingLength normalized) := by - simpa [ExplicitGridPoint] using + simpa only [ExplicitGridPoint, Fintype.card_coe] using GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid_card_pos encodingLength normalized let global : ExplicitConstraintFamily encodingLength normalized := .inl () have hglobal : 0 < explicitFamilyRowCount encodingLength normalized global := by - simpa [global, explicitFamilyRowCount] using hgrid + simpa only [global, explicitFamilyRowCount] using hgrid let actual : assembledBinaryRow (explicitFamilyRowCount encodingLength normalized) degree := ⟨global, (⟨0, hglobal⟩, ⟨0, hdegree⟩)⟩ @@ -3136,13 +3136,9 @@ private theorem paperVariableArityGaussianStructuralAtomOutput_correct encodeAtomic (system.effectiveSquareBasisMatrix row column) := by rw [exactRank] - change - (sourceLatticeStructuralRecords lattice).getD - (2 + lattice.dimension + - row.val * lattice.dimension + column.val) [] = - encodeAtomic (lattice.basis row column) - exact sourceLatticeStructuralRecords_getD_basis - lattice row column + rw [← effectiveGapCVPInstance_basis + system positiveDimension radiusValue radiusPositive row column] + exact sourceLatticeStructuralRecords_getD_basis lattice row column rw [exactRecord] exact atom @@ -3689,9 +3685,7 @@ private theorem paperVariableArityPhysicalFamilyGridCardinalityUnary_eq_actualGr (srcFormula formula)).card true := by rw [paperVariableArityPhysicalFamilyGridCardinalityUnary_valid] congr 1 - simpa only [physGridCard, physFieldCard, physDegree, physicalFormulaSize, - physicalFormulaVariableCount, - paperVariableAritySourceFormula_variableCount] using + exact (sourceFormulaGrid_card_eq_fieldWordCount (encodeThreeCNF formula).length (srcFormula formula)).symm @@ -5739,7 +5733,7 @@ open GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine List.replicate (physicalWordBinarySystem (encodeThreeCNF formula).length formula).rowCount true := by - simpa only [paperVariableArityCanonicalPhysicalMatrixShape_system] using + exact paperCanonicalPhysicalMatrixShape.rowsCorrect formula @[simp] theorem paperVariableArityCanonicalPhysicalMatrixShape_columns_valid @@ -5749,7 +5743,7 @@ open GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine List.replicate (physicalWordBinarySystem (encodeThreeCNF formula).length formula).dimension true := by - simpa only [paperVariableArityCanonicalPhysicalMatrixShape_system] using + exact paperCanonicalPhysicalMatrixShape.columnsCorrect formula /-- GapCVP reduction support. -/ @@ -6529,6 +6523,18 @@ abbrev physicalWordDecodedRow paperVariableArityExplicitBinaryRowWordOrder encodingLength formula row +private theorem binaryFieldParityMatrix_apply_index + {K : Type*} [Field K] [Algebra (ZMod 2) K] + {degree fieldRowCount dimension : ℕ} + (basis : Module.Basis (Fin degree) (ZMod 2) K) + (checks : Matrix (Fin fieldRowCount) (Fin dimension) K) + (index : Fin fieldRowCount × Fin degree) + (column : Fin dimension) : + binaryFieldParityMatrix basis checks index column = + basis.equivFun (checks index.1 column) index.2 := by + rcases index with ⟨row, coordinate⟩ + exact binaryFieldParityMatrix_apply_basisCoordinate basis checks row coordinate column + theorem physicalWordBinaryCheckCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (paperExplicitBinaryRowWordCount @@ -6549,15 +6555,17 @@ theorem physicalWordBinaryCheckCoefficient encodingLength formula row).2.2 := by refine (paperVariableArityPhysicalWordBinarySystem_check_apply encodingLength formula row column).trans ?_ - refine (binaryFieldParityMatrix_apply_basisCoordinate + dsimp only [physicalBinarySystem, + GapCVP.BinaryOrderedAssembly.assembledBinaryAffineSystemOrdered, + assembledBinaryParityMatrix] + with_reducible refine (binaryFieldParityMatrix_apply_index (GapCVP.Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis encodingLength (srcFormula formula)) (sourceFormulaPhysicalFamilyFieldMatrix encodingLength (srcFormula formula) (physicalWordDecodedRow encodingLength formula row).1) - (physicalWordDecodedRow encodingLength formula row).2.1 - (physicalWordDecodedRow encodingLength formula row).2.2 + (physicalWordDecodedRow encodingLength formula row).2 (physicalColumnPermutation encodingLength formula column)).trans ?_ exact congrArg @@ -6602,7 +6610,7 @@ private theorem paperVariableArityPhysicalWordBinaryRightHandSideCoefficient (sourceSizeParameter encodingLength (srcFormula formula)))) coordinate rw [sourceWordValue_oneWord] at word - simpa only [Module.Basis.equivFun_apply, oneWord] using word + exact word private theorem paperVariableArityExplicitFamilyTarget_eq (encodingLength : ℕ) (formula : GapCVP.Core.Formula) @@ -6945,7 +6953,7 @@ theorem paperVariableArityPhysicalRowOrder_global_iff apply (paperExplicitFamilyWordOrder encodingLength formula).injective - simpa only [physicalFamilyWordOrder_zero, List.get_eq_getElem] using selected + exact selected have selectedZero : ((finSigmaFinEquiv (n := paperExplicitBinaryFamilyBlockCount @@ -7669,7 +7677,7 @@ private theorem factor400Irreducible_encodeNat_eq_bits (value : ℕ) : exact Num.to_of_nat value cases numeral with | zero => - have hz : value = 0 := by simpa only [Num.cast_zero'] using hvalue.symm + have hz : value = 0 := by exact hvalue.symm subst value rfl | pos positive => diff --git a/LeanPool/GapCVP/Part14A.lean b/LeanPool/GapCVP/Part14A.lean index 1b1de2110d..5bea0b5cc8 100644 --- a/LeanPool/GapCVP/Part14A.lean +++ b/LeanPool/GapCVP/Part14A.lean @@ -103,7 +103,7 @@ private theorem factor400IndexedIrreducibleCandidateMarkers_findIdxOption id = some rank.val := by rw [factor400IndexedIrreducibleCandidateMarkers_eq_finRange, List.findIdx?_map] - simpa only [CompTriple.comp_eq] using + exact finRange_findIdxOption_of_findOption (fun candidate : Fin (2 ^ degree) => noProperFactors degree (indexedWord degree candidate)) rank hfound @@ -304,7 +304,7 @@ private theorem paperVariableAritySourceIrreducibleRankCoefficientWord_query lengthPrefixedWord (List.replicate rank true) ++ lengthPrefixedWord auxiliary ++ encodeThreeCNF formula from rfl, paperVariableAritySourceIrreducibleCoefficientBitWord_query] - simpa only [degree] using + exact (List.map_eq_flatMap (f := fun bitRank => rank.testBit bitRank) (l := List.range degree)).symm diff --git a/LeanPool/GapCVP/Part14B.lean b/LeanPool/GapCVP/Part14B.lean index fa8f17a7f8..624b4c7f36 100644 --- a/LeanPool/GapCVP/Part14B.lean +++ b/LeanPool/GapCVP/Part14B.lean @@ -1487,16 +1487,11 @@ theorem paperVariableArityPhysicalMatrixGuardedFourFamilyCheck_valid ((physicalWordBinarySystem (encodeThreeCNF formula).length formula).check row column = (1 : ZMod 2))] := by - exact physicalMatrixGuardedFourFamilyCheck_bits global refinement ordinary shifted - (affineCellQuery row.val column.val (encodeThreeCNF formula)) row.val - (physicalFormulaGlobalBoundary formula) - (physicalFormulaRefinementBoundary formula) - (physicalFormulaOrdinaryBoundary formula) - (decide - ((physicalWordBinarySystem - (encodeThreeCNF formula).length formula).check - row column = (1 : ZMod 2))) - correctGlobal correctRefinement correctOrdinary correctShifted + apply physicalMatrixGuardedFourFamilyCheck_bits + · exact correctGlobal + · exact correctRefinement + · exact correctOrdinary + · exact correctShifted private theorem paperVariableArityPhysicalMatrixCheckEntry_transport (source target : GapCVP.Core.BinaryAffineSystem) @@ -2755,8 +2750,7 @@ theorem physicalRefinementGridCard_eq (ExplicitGridPoint (encodeThreeCNF formula).length (srcFormula formula)) = physGridCard formula := by - simpa only [Fintype.card_coe, physGridCard, physFieldCard, physDegree, physicalFormulaSize, - physicalFormulaVariableCount] using physicalSourceGridCardinality_eq (encodeThreeCNF + exact physicalSourceGridCardinality_eq (encodeThreeCNF formula).length formula private theorem paperVariableArityPhysicalRefinementFieldCard_eq @@ -3218,7 +3212,7 @@ private theorem paperVariableArityPhysicalRefinementDecodedFieldRowRank physicalRefinementDegree_pos formula have quotientBound : localRank / degree < grid * field := by apply (Nat.div_lt_iff_lt_mul degreePositive).mpr - simpa only [Nat.mul_assoc] using bounded + exact bounded have sourceRank : row.val - physicalFormulaGlobalBoundary formula = clause.val * (grid * field * degree) + localRank := @@ -4687,8 +4681,7 @@ noncomputable def row column formula hbound)) (paperVariableArityPhysicalColumnGlobalTypeBit_query row column formula) - (by simpa only [physicalRefinementSourceLocalTagInRange, - decide_eq_true_eq] using + (by exact (paperVariableArityPhysicalRefinementLocalTagMarker_query row column formula hbound)) diff --git a/LeanPool/GapCVP/Part15.lean b/LeanPool/GapCVP/Part15.lean index 0e9ef8a9e5..90b2b96cad 100644 --- a/LeanPool/GapCVP/Part15.lean +++ b/LeanPool/GapCVP/Part15.lean @@ -2839,7 +2839,7 @@ theorem change physicalInterpolationNestedDenominatorNodeProductWord width outer = finiteWordBits denominator - simpa only [outer, cell, denominator, Fin.val_castLE] using + exact paperVariableArityPhysicalInterpolationNestedDenominatorNodeProductWord_valid width outerWidth row column formula (Fin.castLE bounded node) count correctWidth bounded @@ -2894,7 +2894,7 @@ theorem (compactPhysicalLagrangeNestedNodeEnvelope outerWidth node.val (affineCellQuery row column (encodeThreeCNF formula))) = _ - simpa only [Fin.val_castLE] using + exact paperVariableArityPhysicalInterpolationNestedNumeratorNodeProductWord_valid family width outerWidth row column formula (Fin.castLE bounded node) count correctWidth bounded @@ -5251,7 +5251,7 @@ private theorem paperVariableArityPhysicalOrdinaryDependentFamilyPrefix formula tag).isLt rw [paperVariableArityPhysicalOrdinaryDependentFamilyIndex_val] at bounded - simpa only [count, familyCount] using bounded + exact bounded have hwhole : 1 + count + tag.val ≤ familyCount := hstrict.le have hfirst : 1 + count ≤ familyCount := by omega let candidate : Fin familyCount := @@ -5694,9 +5694,7 @@ private theorem paperVariableArityPhysicalOrdinaryFamilySourceTypeCardWordRank ((sourceTypeCardWordOrder formula).symm ((paperOrdinaryFamilyWordOrder formula momentBudget tag).1)).val = tag.val / (momentBudget + 1) := by - simpa only [sourceTypeCardWordOrder, Equiv.symm_trans, finCongr_symm, Equiv.trans_apply, - finCongr_apply, - Fin.val_cast] using paperVariableArityPhysicalOrdinaryFamilySourceTypeWordRank formula + exact paperVariableArityPhysicalOrdinaryFamilySourceTypeWordRank formula momentBudget tag private theorem paperVariableArityPhysicalOrdinarySourceRowTypeCardWordRank diff --git a/LeanPool/GapCVP/Part16A.lean b/LeanPool/GapCVP/Part16A.lean index 751cf3aeb5..87e752342c 100644 --- a/LeanPool/GapCVP/Part16A.lean +++ b/LeanPool/GapCVP/Part16A.lean @@ -84,7 +84,7 @@ private theorem paperVariableArityPhysicalOrderedLagrangeParity_eq_selectedCorre intro equality apply hposition have rank := congrArg Fin.val equality - simpa only [Fin.val_castLE] using (rank ▸ node.isLt) + exact (rank ▸ node.isLt) simp only [Nat.succ_eq_add_one, hcast, ↓reduceIte, zero_mul, Finset.sum_const_zero] private theorem paperVariableArityPhysicalOrdinaryMaskedNodeSum_eq_selected @@ -4945,7 +4945,7 @@ private theorem paperVariableArityPhysicalShiftedSourceRowTupleRank_eq (finSigmaFinEquiv.symm tag).1 (finSigmaFinEquiv.symm tag).2).1)).val symm - simpa only [decoded, moment] using + exact paperVariableArityPhysicalShiftedClauseTupleWordRank formula budget decoded.1 decoded.2 @@ -4985,7 +4985,7 @@ private theorem paperVariableArityPhysicalShiftedSourceRowLocalVariableRank_eq (finSigmaFinEquiv.symm tag).1 (finSigmaFinEquiv.symm tag).2).2.1)).val symm - simpa only [decoded, moment] using + exact paperVariableArityPhysicalShiftedClauseLocalVariableWordRank formula budget decoded.1 decoded.2 diff --git a/LeanPool/GapCVP/Part16B.lean b/LeanPool/GapCVP/Part16B.lean index 90db31a1db..1d3769f0d1 100644 --- a/LeanPool/GapCVP/Part16B.lean +++ b/LeanPool/GapCVP/Part16B.lean @@ -854,7 +854,7 @@ private theorem compactPhysicalDecodingBinaryIntegerAtom_of_rational | nil => have hrational : (0 : ℚ) = (value : ℚ) := compactPhysicalDecodingAtomic_injective - (by simpa only [effectiveTargetPackedAtom, markerConditionalOutput] using hatom) + (by exact hatom) have hinteger : value = 0 := by exact_mod_cast hrational.symm simp only [compactPhysicalDecodingBinaryIntegerAtom, markerConditionalOutput, hinteger] @@ -863,14 +863,14 @@ private theorem compactPhysicalDecodingBinaryIntegerAtom_of_rational | false => have hrational : (0 : ℚ) = (value : ℚ) := compactPhysicalDecodingAtomic_injective - (by simpa only [effectiveTargetPackedAtom, markerConditionalOutput] using hatom) + (by exact hatom) have hinteger : value = 0 := by exact_mod_cast hrational.symm simp only [compactPhysicalDecodingBinaryIntegerAtom_false, hinteger] | true => have hrational : (1 : ℚ) = (value : ℚ) := compactPhysicalDecodingAtomic_injective - (by simpa only [effectiveTargetPackedAtom, markerConditionalOutput] using hatom) + (by exact hatom) have hinteger : value = 1 := by exact_mod_cast hrational.symm simp only [compactPhysicalDecodingBinaryIntegerAtom_true, hinteger] @@ -1330,7 +1330,7 @@ private theorem paperVariableArityCodingCheckIntegerFold_valid paperVariableArityCanonicalBinaryMatrixCheckFoldPreparation_valid paperCanonicalPhysicalMatrixShape formula] unfold sourcePhysicalWordPackedQueryPreparation - simpa only [fourFamilyOriginalMarkerStream] using + exact boundedRecordFoldOutput_sourceFourFamilyOriginalMarkerQueries (paperCodingCheckIntegerMarker worker) (paperCanonicalBinaryMatrixCheckQueries paperCanonicalPhysicalMatrixShape formula) @@ -1350,7 +1350,7 @@ private theorem paperVariableArityCodingRhsIntegerFold_valid paperVariableArityCanonicalBinaryMatrixRhsFoldPreparation_valid paperCanonicalPhysicalMatrixShape formula] unfold sourcePhysicalWordPackedQueryPreparation - simpa only [fourFamilyOriginalMarkerStream] using + exact boundedRecordFoldOutput_sourceFourFamilyOriginalMarkerQueries (paperCodingRhsIntegerMarker worker) (paperCanonicalBinaryMatrixRhsQueries paperCanonicalPhysicalMatrixShape formula) @@ -1410,7 +1410,7 @@ private theorem paperVariableArityCodingRhsIntegerPayload_valid (encodeThreeCNF formula).length formula).dimension := ⟨0, paperCanonicalPhysicalMatrixShape.columnsPositive formula⟩ - simpa only [ZMod.natCast_val] using + exact paperVariableArityCodingRhsIntegerMarker_valid worker formula row column diff --git a/LeanPool/GapCVP/Part17.lean b/LeanPool/GapCVP/Part17.lean index f08f58daa4..ec0476b511 100644 --- a/LeanPool/GapCVP/Part17.lean +++ b/LeanPool/GapCVP/Part17.lean @@ -1017,7 +1017,7 @@ private theorem paperVariableArityFinitePRadiusAtomicOutput_valid (encodeThreeCNF formula).length formula)) (finitePRadiusScale_pos p hp) (paperVariableArityFinitePNumeratorUnary_valid p hp formula) - simpa only [finitePRadius] using physical + exact physical /-- Assemble the finite-p physical source word from the Gaussian matrix and radius data. -/ noncomputable def paperFinitePPhysicalStructuralOutput @@ -1067,7 +1067,7 @@ private theorem paperVariableArityFinitePPhysicalStructuralOutput_valid (paperVariableArityFinitePRadiusAtomicOutput_valid p hp formula) (gaussianPaperVariableArityCanonicalSourceReducedStateOutput_effective cell formula) - simpa only [paperFinitePPhysicalFormulaInstance, paperFinitePPhysicalSystem] using physical + exact physical /-- Route the source to the canonical or structural finite-p output according to its guards. -/ def paperFinitePPhysicalRoutedOutput