The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 21 Feb 2013 23:04:15 +0100,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 a écrit :

> Hello.
> 
> A few months ago I asked about decidable equality on nested
> structures. As usual, Cedric Auger came to the rescue :)

Well, being named, I felt I had to reply (although two persons already
gave a solution)…

I give here a solution which does not change data types (end of the
mail).
There is some alternative with embedding the list in the inductive type.

Inductive box : Type :=
 Cons : nat → list_box → box
with list_box : Type :=
  nil_box : list_box
| cons_box : box → list_box → list_box
.

Which I find simpler to use (but you may need to redefine some stuff of
the basic List library, such as In, that you require for your 'p')

With such a definition, a

Lemma Lbox : ∀ b, P b
with Llist_box : ∀ lb, Q lb.
Proof.
…
Qed.

Where P and Q are what you want, is rather easy to use.
(Do it one time to try…)

Just a warning: the "Lemma … with …" puts you in a "fix" context, for
which you have to be careful with guardedness (generally not too much
hard to deal with, but just keep it in mind).

> 
> Here's the log about the thread in question:
> https://sympa.inria.fr/sympa/arc/coq-club/2012-08/msg00122.html
> 
> Anyway, I believe i have a similar problem now, but I'm not sure how I
> could adapt the approach to solve my particular situation.
> 
> Say you have an inductive like so:
> 
> Inductive box : Type :=
>   Cons : nat -> list box -> box.
> 
> And now I want to prove
> 
> Lemma p_dec:
>   forall b:box, p b \/ ~ p b.
> 
> where p is some predicate of the following shape:
> 
> Inductive p (b:box) : Prop :=
>  | Xyz : forall n lb, b = Cons n lb ->
>                              (forall b', In b' lb -> p b') ->
>                              q n.
> 
> 
> So, in order to prove p_dec I would need decidability on predicate q
> (which you can assume I have), but also decidability on all b' for
> p....So you see my problem here :-)
> 
> I believe the solution will be something similar to the one on
> decidable equality shown on the link above...but how can I adapt it
> to my case?
> 
> Cheers!
> 
> 

Require Import Utf8.
Require Import List.

Inductive box : Type :=
  Cons : nat → list box → box.

Axiom q : nat → Prop.

Axiom Hq : ∀ n, q n ∨ ¬ q n.

Inductive p (b:box) : Prop :=
 | Xyz : ∀ n lb,
         b = Cons n lb →
         (∀ b', In b' lb -> p b') →
         q n →
         p b (*Well, I guess it required to be corrected this way*).

Definition dec (P : Prop) := P ∨ ¬ P.

Lemma p_nil_dec : dec (∀ b', In b' nil → p b').
Proof. left; intros b' []. Qed.

Lemma p_cons_dec b (Hb  : dec (p b))
                lb (Hlb : dec (∀ b', In b' lb → p b'))
: dec (∀ b', In b' (cons b lb) → p b').
Proof.
  simpl.
  destruct Hb as [Hb|Hb]; [|clear Hlb].
    destruct Hlb as [Hlb|Hlb]; [|clear Hb].
      left; intros b' [Heq|HIn]; subst; auto.
    right; intros Habs; apply Hlb; clear Hlb.
    intros b' Hb'; apply Habs; right; auto.
  right; intros Habs; apply Hb; clear Hb.
  apply Habs; left; auto.
Qed.

Lemma p_lb_dec (Hp : ∀ b, p b ∨ ¬ p b)
: ∀ lb, (∀ b', In b' lb → p b') ∨ ¬ (∀ b', In b' lb → p b').
Proof.
  exact (fix p_lb_dec lb :=
         match lb with
         | nil => p_nil_dec
         | cons b lb => p_cons_dec b (Hp b) lb (p_lb_dec lb)
         end).
(* Qed. (* Hides recursion to the caller, so don't do it! *) *)
Defined. (* AND NOT Qed! *)

Lemma p_dec: ∀ b:box, p b ∨ ¬ p b.
Proof.
  fix 1; intros [n lb].
  assert (IHp_dec := p_lb_dec p_dec lb); clear p_dec.
  Guarded. (* strangely, it does not fail when Qed is used. Bug? *)
  (* Thanks to Defined instead of Qed, guardedness is checkable *)
  (* Now that p_dec has been cleared,
     the 'fix' tactic previously used has become harmless *)
  destruct (Hq n) as [q_n|Not_q_n]; [|clear IHp_dec].
    destruct IHp_dec as [IHp|Not_IHp]; [|clear q_n].
      left; split with n lb; auto.
    right; intros [n_ lb_ Heq Hlb_ _]; apply Not_IHp; clear Not_IHp.
    inversion Heq; clear - Hlb_.
    auto.
  right; intros [n_ lb_ Heq _ Hn_]; apply Not_q_n; clear Not_q_n.
  inversion Heq; clear - Hn_.
  auto.
Qed.
(*
Some remarks :
→ p_nil_dec and p_cons_dec could have been defined inside p_lb_dec, but:
  → proving it directly would have lead to a big term due to Defined
    instead of Qed
  → using the abstract tactic would have done the same result as what
    we did here (well, modulo the names of auxiliary lemmas),
    but writing proofs under "abstract" is all but convenient
    (I generally do it without abstract, and then use ";" and "[", "|",
    "]" to get a one tactic proof, so that is not maintainable…)
→ For p_lb_dec, I did not tried the "induction" tactic. I do not know if
  it works with it (Well, in fact I do not know if "list_ind" is or is
  not opaque. Provided it is transparent, it should work, else it should
  not.) That was just to show the recursive structure of the proof (and
  how simple the term is with the auxiliary lemmas)
→ p_dec is not directly provable with "induction", so I used fix, and my
  usual trick to deal with it: generalize on the recursive call, and
  immediately after clear the fixpoint, and run "Guarded", so that
  for the rest you will be safe ("fix" won't annoy you anymore).
→ I use a lot the "clear" tactic. It is often not mandatory and you can
  safely remove it (well, except for the "clear p_dec.", although you
  can remove it, I do not advise to do so, as it can quickly break proof
  scripts). I just used them to have rather nice contexts, nothing more.
*)