pedro.lean

pedro.lean

import control.bifunctor
import data.multiset.basic
import tactic

example {α} {x : α} {xs : multiset α} : {x} ≤ x :: xs :=
begin
  rw multiset.singleton_eq_singleton,
  apply multiset.cons_le_cons,
  apply zero_le,
end

universe u

@[derive decidable_eq]
inductive term : Type
| var : ℕ → term
| impl : term → term → term

open term
namespace term

def weight : term → ℕ
| (var _) := 1
| (impl x y) := x.weight + y.weight + 1

instance : has_lt term := ⟨inv_image (<) weight⟩

def wf_term : well_founded ((<) : term → term → Prop) := measure_wf _

end term

@[derive [has_add]]
def dm (α) := multiset α

instance {α : Type u} [decidable_eq α] : has_sub (dm α) :=
⟨λ X Y, (X - Y : multiset α)⟩

def to_dm {α} (s : multiset α) : dm α := s

instance {α : Type u} [decidable_eq α] [has_lt α] : has_lt (dm α) :=
{ lt := λ M N, ∃ (X Y : multiset α), X ≠ 0 ∧ (X : multiset α) ≤ (N : multiset α) ∧ M = (N - X) + Y ∧ ∀ y ∈ Y, ∃ x ∈ X, y < x }

-- standard result about the Dershowitz–Manna ordering
lemma wf_dm {α : Type u} [decidable_eq α] [has_lt α] (t : well_founded ((<) : α → α → Prop)) :
  well_founded ((<) : dm α → dm α → Prop) :=
sorry

def select {α : Type u} : list α → list (α × list α)
| (a :: as) := (a, as) :: list.map (bifunctor.snd (list.cons a)) (select as)
| [] := []

#check inv_image

def combine : (Σ' (a : list term), term) → list term := λ ⟨xs, x⟩, x :: xs

def args_to_dm : (Σ' (a : multiset term), term) → dm term :=
λ x, to_dm (x.2 :: x.1)

def my_ordering : (Σ' (a : multiset term), term) → (Σ' (a : multiset term), term) → Prop :=
inv_image (<) args_to_dm

lemma proof2 (a b env) : my_ordering ⟨a :: env, b⟩ ⟨env, a.impl b⟩ :=
begin
  change to_dm (b :: a :: env) < to_dm (a.impl b :: env),
  refine ⟨a.impl b :: 0, b :: a :: 0, _, _, _, _⟩,
  { simp },
  { apply multiset.cons_le_cons,
    apply zero_le },
  { change b :: a :: env = a.impl b :: env - _ + _,
    simp },
  { simp only [exists_prop, multiset.mem_cons, exists_eq_left, multiset.mem_singleton],
    rintro _ (rfl | rfl);
    change _ < _ + _;
    linarith },
end

example {α} (x y : α) (xs : multiset α) : x :: y :: xs = y :: x :: xs :=
begin
  refine multiset.cons_swap x y xs,
end

lemma proof3 (env : multiset term) (x y : ℕ) (a b : term) (e' : multiset term)
  (h₁ : a.impl b :: e' = env) (h₂ : a = var y) (h₃ : a ∈ e') :
my_ordering ⟨b :: e', var x⟩ ⟨env, var x⟩ :=
begin
  subst h₂,
  subst h₁,
  refine ⟨(var y).impl b :: 0, b :: 0, _, _, _, _⟩,
  { simp },
  { change multiset.cons _ _ ≤ multiset.cons (var x) (_ :: _),
    simp },
  { change var x :: b :: e' = (_ :: _ :: _) - (_ :: _) + (b :: 0),
    simp [multiset.cons_swap (var x) b] },
  { simp only [exists_prop, forall_eq, exists_eq_left, multiset.mem_singleton],
    change _ < _ + _,
    linarith }
end

lemma proof4 (env : multiset term) (a b c d : term) (e' : multiset term) (x : ℕ)
  (h₁ : a.impl b :: e' = env) (h₂ : a = c.impl d) :
my_ordering ⟨d.impl b :: e', a⟩ ⟨env, var x⟩ :=
begin
  subst h₁,
  subst h₂,
  change multiset.cons _ (multiset.cons _ _) < multiset.cons _ _,
  dsimp,
  refine ⟨var x :: (c.impl d).impl b :: 0, c.impl d :: d.impl b :: 0, _, _, _, _⟩,
  { simp },
  { apply multiset.cons_le_cons, apply multiset.cons_le_cons, apply zero_le },
  { simp },
  { simp only [exists_prop, multiset.mem_cons, multiset.mem_singleton],
    rintro _ (rfl | rfl),
    { refine ⟨_, or.inr rfl, _⟩,
      change _ < _ + _,
      linarith },
    { refine ⟨_, or.inr rfl, _⟩,
      change _ + _ < (_ + _) + _ + _,
      linarith } },
end

lemma proof4' (e' env : multiset term) (a b c d : term) (x : ℕ) (h₁ : a.impl b :: e' = env) (h₂ : a = c.impl d) :
  my_ordering ⟨b :: e', var x⟩ ⟨env, var x⟩ :=
begin
  subst h₂,
  subst h₁,
  change multiset.cons _ (multiset.cons _ _) < multiset.cons _ _,
  dsimp,
  refine ⟨(c.impl d).impl b :: 0, b :: 0, _, _, _, _⟩,
  { simp },
  { simp },
  { simp [multiset.cons_swap] },
  { simp only [exists_prop, forall_eq, exists_eq_left, multiset.mem_singleton],
    change _ < _ + _,
    linarith }
end

def ljt' : multiset term → term → Prop
| env t@(var x) :=
    if t ∈ env  -- LJT₁ for A = var _
      then true
      else ∃ a b (e' : multiset term) (h₁ : impl a b :: e' = env),  -- split env up: this is another way of doing `select`
             ((∃ y (h₂ : a = var y) (h₃ : a ∈ e'), (have my_ordering ⟨b :: e', var x⟩ ⟨env, var x⟩, from proof3 _ _ _ _ _ _ h₁ h₂ h₃, ljt' (b :: e') t)) ∨ -- LJT₃
              (∃ c d (h₂ : a = impl c d),
                (have my_ordering ⟨d.impl b :: e', a⟩ ⟨env, var x⟩, from proof4 _ _ _ _ _ _ _ h₁ h₂, ljt' (impl d b :: e') a) ∧
                 have my_ordering ⟨b :: e', var x⟩ ⟨env, var x⟩, from proof4' _ _ _ _ _ _ _ h₁ h₂, ljt' (b :: e') t)) -- the two new parts of LJT₄
| env t@(impl a b) :=
  if t ∈ env -- LJT₁ for A = impl _ _
    then true
    else have my_ordering ⟨a :: env, b⟩ ⟨env, a.impl b⟩, from proof2 a b env,
              ljt' (a :: env) b -- LJT₂ (use proof2)
using_well_founded
  { rel_tac := λ _ _, `[exact ⟨my_ordering, inv_image.wf _ (wf_dm term.wf_term)⟩],
    dec_tac := tactic.assumption}