# Zulip Chat Archive

## 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')
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 (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')
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 (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,
{ 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 (Nov 14 2020 at 20:38):

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.

Last updated: May 13 2021 at 18:26 UTC