b5122b6a7b
This change * moves `termination_by` and `decreasing_by` next to the function they apply to * simplify the syntax of `termination_by` * apply the `decreasing_by` goal to all goals at once, for better interactive use. See the section in `RELEASES.md` for more details and migration advise. This is a hard breaking change, requiring developers to touch every `termination_by` in their code base. We decided to still do it as a hard-breaking change, because supporting both old and new syntax at the same time would be non-trivial, and not save that much. Moreover, this requires changes to some metaprograms that developers might have written, and supporting both syntaxes at the same time would make _their_ migration harder.
59 lines
2 KiB
Text
59 lines
2 KiB
Text
inductive Term
|
||
| Var (i : Nat)
|
||
| Cons (l : Term) (r : Term)
|
||
|
||
def Subst := Nat → Nat
|
||
|
||
def depth : Term → Nat
|
||
| .Var _ => 0
|
||
| .Cons l r => 1 + depth l + depth r
|
||
|
||
def act (f : Subst) (t : Term) := match t with
|
||
| .Var i => Term.Var (f i)
|
||
| .Cons l r => Term.Cons (act f l) (act f r)
|
||
|
||
def strangers (u v : Term) := ∀ f : Subst, act f u ≠ act f v
|
||
|
||
abbrev P (c : Option Subst) u v := match c with
|
||
| none => strangers u v
|
||
| some f => act f u = act f v
|
||
|
||
instance rel : WellFoundedRelation (Term × Term) := measure (λ (u, v) => depth u + depth v)
|
||
|
||
theorem decr_left (l₁ r₁ l₂ r₂ : Term) :
|
||
rel.rel (l₁, l₂) (Term.Cons l₁ r₁, Term.Cons l₂ r₂) := by
|
||
suffices h : depth l₁ + depth l₂ < depth (Term.Cons l₁ r₁) + depth (Term.Cons l₂ r₂) from h
|
||
admit
|
||
|
||
theorem decr_right (l₁ r₁ l₂ r₂ : Term) (f : Subst) :
|
||
rel.rel (act f r₁, act f r₂) (Term.Cons l₁ r₁, Term.Cons l₂ r₂) := by
|
||
suffices h : depth (act f r₁) + depth (act f r₂) < depth (Term.Cons l₁ r₁) + depth (Term.Cons l₂ r₂) from h
|
||
admit
|
||
|
||
def robinson (u v : Term) : { f : Option Subst // P f u v } := match u, v with
|
||
| .Cons l₁ r₁, .Cons l₂ r₂ => match robinson l₁ l₂ with
|
||
| ⟨ none, h ⟩ => ⟨ none, sorry ⟩
|
||
| ⟨ some f, h ⟩ => match robinson (act f r₁) (act f r₂) with
|
||
| ⟨ none, h ⟩ => ⟨ none, sorry ⟩
|
||
| ⟨ some g, h ⟩ => ⟨ some (g ∘ f), sorry ⟩
|
||
| .Var i, .Cons l r => ⟨ none, sorry ⟩
|
||
| .Cons l r, .Var i => ⟨ none, sorry ⟩
|
||
| .Var i, .Var j =>
|
||
if i = j then ⟨ some id, sorry ⟩
|
||
else ⟨ some λ n => if n = i then j else n, sorry ⟩
|
||
termination_by (u, v)
|
||
decreasing_by
|
||
· apply decr_left _ _ _ _
|
||
· apply decr_right _ _ _ _ _
|
||
|
||
attribute [simp] robinson
|
||
|
||
set_option pp.proofs true
|
||
#check robinson._eq_1
|
||
#check robinson._eq_2
|
||
#check robinson._eq_3
|
||
#check robinson._eq_4
|
||
|
||
theorem ex : (robinson (Term.Var 0) (Term.Var 0)).1 = some id := by
|
||
unfold robinson
|
||
admit
|