## Stream: new members

### Topic: Reasoning with inductive relations

#### Thorsten Altenkirch (Nov 13 2020 at 12:44):

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')

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 (Nov 13 2020 at 13:10):

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 (Nov 13 2020 at 13:32):

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 (Nov 13 2020 at 15:14):

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')

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 (Nov 13 2020 at 15:27):

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,