ExtensionExamples.lean

1 import ProofPath.Transport
2 import ProofPath.Recovery
3 
4 namespace ProofPath
5 namespace ExtensionExamples
6 
7 def conjunction : Field (Fin 3) Unit where
8   leaf := ∅
9   premises _ := {0, 1}
10   conclusion _ := 2
11   certified _ := True
12 
13 theorem forbidden_two_derived : (2 : Fin 3) ∈ conjunction.closure {0, 1} := by
14   apply Field.Derives.step () trivial
15   intro v hv
16   exact conjunction.closure_contains_seed {0, 1} hv
17 
18 theorem conjunction_obstructed :
19     ¬ ∃ x, conjunction.Extends {0, 1} {2} x := by
20   apply (conjunction.infeasible_iff_forbidden_derivation _ _).mpr
21   exact ⟨2, by simp, forbidden_two_derived⟩
22 
23 theorem partial_a_false_c_feasible :
24     ∃ x, conjunction.Extends {0} {2} x := by
25   refine ⟨fun v => v = 0, ⟨?_, ?_⟩, ?_, ?_⟩
26   · intro v hv
27     exact False.elim hv
28   · intro _ _ hp
29     have h : (1 : Fin 3) = 0 := hp 1 (by simp [conjunction])
30     exact False.elim ((by decide : (1 : Fin 3) ≠ 0) h)
31   · intro v hv
32     exact Set.mem_singleton_iff.mp hv
33   · intro v hv
34     have h : v = 2 := Set.mem_singleton_iff.mp hv
35     rw [h]
36     decide
37 
38 def source : Field Bool Empty where
39   leaf := ∅
40   premises := Empty.elim
41   conclusion := Empty.elim
42   certified := Empty.elim
43 
44 def target : Field Unit Empty where
45   leaf := ∅
46   premises := Empty.elim
47   conclusion := Empty.elim
48   certified := Empty.elim
49 
50 def collapse : RuleTransport source target where
51   node _ := ()
52   rule := Empty.elim
53   leaves := by intro _ h; exact False.elim h
54   certified := by intro j; exact Empty.elim j
55   premises := by intro j; exact Empty.elim j
56   conclusion := by intro j; exact Empty.elim j
57 
58 theorem source_feasible : ∃ x, source.Extends {false} {true} x := by
59   refine ⟨fun b => b = false, ⟨?_, ?_⟩, ?_, ?_⟩
60   · intro v h; exact False.elim h
61   · intro j; exact Empty.elim j
62   · intro v hv; exact Set.mem_singleton_iff.mp hv
63   · intro v hv
64     have h : v = true := Set.mem_singleton_iff.mp hv
65     rw [h]
66     decide
67 
68 theorem collapsed_target_infeasible :
69     ¬ ∃ x, target.Extends (collapse.node '' {false}) (collapse.node '' {true}) x := by
70   rintro ⟨x, hx⟩
71   exact hx.2.2 () ⟨true, by simp, rfl⟩ (hx.2.1 () ⟨false, by simp, rfl⟩)
72 
73 end ExtensionExamples
74 end ProofPath

Back to source controls