TraceFixtures.lean

1 import ProofPath.TraceWire
2 
3 /-! Generated concrete records. Acceptance is kernel-normalized with decide;
4 not inferred from Python's PASS flag. JSON text and address books remain in
5 examples/trace_exchange for independent input correspondence checks. -/
6 namespace ProofPath.Trace.Fixtures
7 open Wire
8 
9 def andPositiveProblem : Problem := ⟨8, [0], [⟨[7], 1⟩, ⟨[4], 2⟩, ⟨[0], 3⟩, ⟨[3], 4⟩, ⟨[0, 3], 6⟩, ⟨[6], 7⟩], [], []⟩
10 def andPositiveCertificate : Certificate := ⟨true, [0, 1, 2, 3, 4, 6, 7], [2, 3, 4, 5, 0, 1], none⟩
11 theorem andPositive_accepted : accept andPositiveProblem andPositiveCertificate = true := by decide
12 theorem andPositive_checked : CertifiedAnswer andPositiveProblem andPositiveCertificate :=
13   acceptance_sound _ _ andPositive_accepted
14 
15 def andNegativeProblem : Problem := ⟨8, [0], [⟨[7], 1⟩, ⟨[4], 2⟩, ⟨[0], 3⟩, ⟨[3], 4⟩, ⟨[0, 3], 6⟩, ⟨[6], 7⟩], [], [1]⟩
16 def andNegativeCertificate : Certificate := ⟨false, [0, 1, 2, 3, 4, 6, 7], [2, 3, 4, 5, 0, 1], some ⟨1, [2, 4, 5, 0]⟩⟩
17 theorem andNegative_accepted : accept andNegativeProblem andNegativeCertificate = true := by decide
18 theorem andNegative_checked : CertifiedAnswer andNegativeProblem andNegativeCertificate :=
19   acceptance_sound _ _ andNegative_accepted
20 
21 def alternativePositiveProblem : Problem := ⟨4, [0], [⟨[2], 1⟩, ⟨[3], 1⟩, ⟨[0], 2⟩, ⟨[0], 3⟩], [], []⟩
22 def alternativePositiveCertificate : Certificate := ⟨true, [0, 1, 2, 3], [2, 3, 0], none⟩
23 theorem alternativePositive_accepted : accept alternativePositiveProblem alternativePositiveCertificate = true := by decide
24 theorem alternativePositive_checked : CertifiedAnswer alternativePositiveProblem alternativePositiveCertificate :=
25   acceptance_sound _ _ alternativePositive_accepted
26 
27 def alternativeNegativeProblem : Problem := ⟨4, [0], [⟨[2], 1⟩, ⟨[3], 1⟩, ⟨[0], 2⟩, ⟨[0], 3⟩], [], [1]⟩
28 def alternativeNegativeCertificate : Certificate := ⟨false, [0, 1, 2, 3], [2, 3, 0], some ⟨1, [2, 0]⟩⟩
29 theorem alternativeNegative_accepted : accept alternativeNegativeProblem alternativeNegativeCertificate = true := by decide
30 theorem alternativeNegative_checked : CertifiedAnswer alternativeNegativeProblem alternativeNegativeCertificate :=
31   acceptance_sound _ _ alternativeNegative_accepted
32 
33 def seededCycleProblem : Problem := ⟨2, [], [⟨[0], 1⟩, ⟨[1], 0⟩], [0], [1]⟩
34 def seededCycleCertificate : Certificate := ⟨false, [0, 1], [0], some ⟨1, [0]⟩⟩
35 theorem seededCycle_accepted : accept seededCycleProblem seededCycleCertificate = true := by decide
36 theorem seededCycle_checked : CertifiedAnswer seededCycleProblem seededCycleCertificate :=
37   acceptance_sound _ _ seededCycle_accepted
38 
39 def emptyProblemProblem : Problem := ⟨0, [], [], [], []⟩
40 def emptyProblemCertificate : Certificate := ⟨true, [], [], none⟩
41 theorem emptyProblem_accepted : accept emptyProblemProblem emptyProblemCertificate = true := by decide
42 theorem emptyProblem_checked : CertifiedAnswer emptyProblemProblem emptyProblemCertificate :=
43   acceptance_sound _ _ emptyProblem_accepted
44 
45 end ProofPath.Trace.Fixtures

Back to source controls