Reasoning with inductive relations

Stream: new members

[Thorsten Altenkirch]

I am trying to translate an agda proof (about permutations) to Lean but I find this rather difficult even though I know how to do it in principle. Hence I wonder wether there is any tactic support I miss or any general advice?

Here is my agda code:

open import Data.List
open import Data.Product

variable A : Set
variable a b : A
variable as bs cs : List A

data Add : A → List A → List A → Set where
  zero : Add a as (a ∷ as)
  suc : Add a as bs → Add a (b ∷ as) (b ∷ bs)

addLem : Add a as bs → Add b bs cs
       → Σ (List A) (λ ds → Add b as ds × Add a ds cs)
addLem zero zero = _ , zero , suc zero
addLem zero (suc q) = _ , q , zero
addLem (suc p) zero = _ , zero , suc (suc p)
addLem (suc p) (suc q) with addLem p q
...                      |  bs' , p' , q' = _ , suc p' , suc q'

and here are the corresponding Lean definitions:

variable {A : Type}

open list

inductive Add : A → list A → list A → Prop
| add_zero : ∀ a:A, ∀ as : list A,Add a as (a :: as)
| add_succ : ∀ a b:A, ∀ as as': list A, Add a as as' → Add a (b :: as) (b :: as')

open Add

variables as bs cs as' cs' : list A
variables a b : A

lemma add_lem : Add a as bs → Add b bs cs → ∃ ds : list A, Add b as ds ∧ Add a ds cs :=
begin
  sorry
end

So I try to translate the proof using pattern matching and structural recursion into just using the induction tactic. This is a bit a dejavue from my PhD ... I remember this was one of the reasons I never seriously used Coq, but Lean doesn't seem any better if not worse because in coq there is Matthieu Sozeau's equations package which I think would enable me to do the agda proof in coq (haven't tried it).

[Anne Baanen]

The induction tactic has some limitations, most notably that it tends to forget what you applied it to. @Jannis Limperg, am I right that your improved induction' will work here?

[Jannis Limperg]

Yes. induction' is partly a reimplementation of Conor's Depelim, which helps a lot with indexed families. It's very similar to Coq's dependent induction and the Equations package is built on the same tech afaik. Let me try what induction' says in this example...

[Jannis Limperg]

Slightly embarrassingly, I'm failing to do the induction' proof right now. The problem is with the double induction, which induction tactics don't do well. I'll try again later. For the moment, here's the Agda-style proof transcribed to Lean, using the equation compiler:

variable {A : Type}

open list

inductive Add : A → list A → list A → Prop
| add_zero : ∀ a:A, ∀ as : list A, Add a as (a :: as)
| add_succ : ∀ a b:A, ∀ as as': list A, Add a as as' → Add a (b :: as) (b :: as')

open Add

lemma add_lem₁ : ∀ {a b as bs cs},
  Add a as bs → Add b bs cs → ∃ ds : list A, Add b as ds ∧ Add a ds cs
| _ _ _ _ _ (add_zero a as) (add_zero b bs) :=
  ⟨b :: as, add_zero _ _, add_succ _ _ _ _ (add_zero _ _)⟩
| _ _ _ _ _ (add_zero a as) (add_succ a' b as' as'' p) :=
  ⟨as'', p, add_zero _ _⟩
| _ _ _ _ _ (add_succ a b as as' p) (add_zero b' bs) :=
  ⟨b' :: b :: as, add_zero _ _, add_succ _ _ _ _ (add_succ _ _ _ _ p)⟩
| _ _ _ _ _ (add_succ a b as as' p) (add_succ a₀ b₀ as₀ as'₀ q) :=
  let ⟨ds', p', q'⟩ := add_lem₁ p q in
  ⟨b₀ :: ds', add_succ _ _ _ _ p', add_succ _ _ _ _ q'⟩

[Mario Carneiro]

Here's a version using the induction tactic:

import tactic

variable {A : Type}

open list

inductive Add : A → list A → list A → Prop
| zero {a:A} {as : list A} : Add a as (a :: as)
| succ {a b:A} {as as': list A} : Add a as as' → Add a (b :: as) (b :: as')

variables as bs cs as' cs' : list A
variables a b : A

lemma add_lem : Add a as bs → Add b bs cs → ∃ ds : list A, Add b as ds ∧ Add a ds cs :=
begin
  intros h1 h2,
  generalize_hyp e : bs = bs' at h2,
  induction h1 with _ _ _ _ _ _ p generalizing cs bs';
    induction h2 with _ _ _ _ _ _ q; cases e,
  { exact ⟨_, Add.zero, Add.zero.succ⟩ },
  { exact ⟨_, q, Add.zero⟩ },
  { exact ⟨_, Add.zero, p.succ.succ⟩ },
  { obtain ⟨bs', p', q'⟩ := h1_ih _ _ rfl q,
    exact ⟨_, p'.succ, q'.succ⟩ },
end

[Thorsten Altenkirch]

Thanks for the helpful comments. Yes, I was wondering wether the easiest way would be to just use the equations compiler. However, I avoided talking about proof terms in my undergraduate course (maybe this is a mistake), hence a tactic based proof like the one by @Mario Carneiro fits the bill perfectly. I need to study it in more detail and hopefully I will be able to translate the rest of my proof.

[Thorsten Altenkirch]

Jannis Limperg said:

Slightly embarrassingly, I'm failing to do the induction' proof right now. The problem is with the double induction, which induction tactics don't do well. I'll try again later. For the moment, here's the Agda-style proof transcribed to Lean, using the equation compiler:

variable {A : Type}

open list

inductive Add : A → list A → list A → Prop
| add_zero : ∀ a:A, ∀ as : list A, Add a as (a :: as)
| add_succ : ∀ a b:A, ∀ as as': list A, Add a as as' → Add a (b :: as) (b :: as')

open Add

lemma add_lem₁ : ∀ {a b as bs cs},
  Add a as bs → Add b bs cs → ∃ ds : list A, Add b as ds ∧ Add a ds cs
| _ _ _ _ _ (add_zero a as) (add_zero b bs) :=
  ⟨b :: as, add_zero _ _, add_succ _ _ _ _ (add_zero _ _)⟩
| _ _ _ _ _ (add_zero a as) (add_succ a' b as' as'' p) :=
  ⟨as'', p, add_zero _ _⟩
| _ _ _ _ _ (add_succ a b as as' p) (add_zero b' bs) :=
  ⟨b' :: b :: as, add_zero _ _, add_succ _ _ _ _ (add_succ _ _ _ _ p)⟩
| _ _ _ _ _ (add_succ a b as as' p) (add_succ a₀ b₀ as₀ as'₀ q) :=
  let ⟨ds', p', q'⟩ := add_lem₁ p q in
  ⟨b₀ :: ds', add_succ _ _ _ _ p', add_succ _ _ _ _ q'⟩

Hi Jannis,

I am having problems loading this proof into lean. It says that the equation compiler failed. Is this a version issue or is there something wrong with my lean installation?

Cheers,
Thorsten

[Kevin Buzzard]

That file compiles fine for me with Lean (version 3.48.0, commit 283f6ed8083a, Release)