Zulip Chat Archive

Stream: new members

Topic: Reasoning with inductive relations


view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip 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