The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

On Tue, Dec 9, 2014 at 11:34 PM, Frédéric Blanqui frederic.blanqui-at-inria.fr |coq-club/Example Allow| <rm7qvfy1wt AT sneakemail.com> wrote:

Hello.

Le 10/12/2014 01:53, Saulo Araujo a écrit :

Hi,

I need to compare values of the type PATH defined below

Definition ID := string.

Inductive STEP : Type :=
  | LastStep : ID -> STEP | Step : ID -> PATH -> STEP | Init : ID -> STEP
with PATH : Type := Path : list STEP -> PATH.

Is there a way to compare those values in Gallina like we compare them in SML?

I tried the suggestion in http://stackoverflow.com/questions/6636131/searching-through-a-list-recursively-in-coq

Definition PATH_dec : forall x y : ID, {x = y} + {x <> y}.

I guess you want x y : PATH instead...

Proof. decide equality. Defined.

To prove this, you need to proceed by induction on PATH. Unfortunately, the induction principle automatically generated by Coq is not correct because Coq does not recognize the argument of Path as recursive. But you can redefine it yourself by using "fix". See for instance the file Term/Varyadic/VTerm.html in http://color.inria.fr (http://color.inria.fr/doc/CoLoR..Term.Varyadic.VTerm.html does not contain proofs). You also need list_eq_dec and string_dec in the List and String modules.

Section 14.3.3 of Coq'Art also discusses this.

I'm curious if anyone has a more compact (but still readable) proof.

Require Import Coq..Strings.String.

Definition ID := string.

Inductive STEP : Type :=
  | LastStep : ID -> STEP | Step : ID -> PATH -> STEP | Init : ID -> STEP
with PATH : Type := Path : list STEP -> PATH.

Section STEP_ind2.

Variables
    (P: STEP -> Type)
    (Q: PATH -> Type)
    (R: list STEP -> Type).

Hypotheses
    (HLastStep: forall (i:ID), P (LastStep i))
    (HStep: forall (i:ID)(p:PATH), Q p -> P (Step i p))
    (HInit: forall (i:ID), P (Init i)).

Hypotheses
    (HPath: forall (l:list STEP), R l -> Q (Path l)).

Hypotheses
    (Hnil: R nil)
    (Hcons: forall s:STEP, P s ->
        forall l:list STEP, R l -> R (cons s l)).

Fixpoint STEP_ind2 (s:STEP) : P s :=
  match s as x return P x with
  | LastStep i => HLastStep i
  | Step i p => HStep i p
    (
      match p as x return Q x with
      | Path l => HPath l
        (
          (fix l_ind (l':list STEP) : R l' :=
            match l' as x return R x with
            | nil => Hnil
            | cons h t => Hcons h (STEP_ind2 h) t (l_ind t)
            end
          ) l
        )
      end
    )
  | Init i => HInit i
  end.
End STEP_ind2.

Local Hint Constructors STEP.

Definition STEP_dec : forall x y : STEP, {x = y} + {x <> y}.
Proof.
  intro x.
  induction x using STEP_ind2 with
      (Q:=fun p => forall p2, {p = p2} + {p <> p2})
      (R:=fun l => forall l2, {l = l2} + {l <> l2}).
  - (* Prove eq_dec for LastStep *)
    destruct y; try (right; intro H; discriminate H).
    (* One subgoal left, which is where both are LastStep *)
    destruct (string_dec i i0); subst.
    + auto.
    + right.
      intro H.
      contradiction n.
      injection H.
      tauto.
  - (* Prove eq_dec for Step *)
    destruct y; try (right; intro H; discriminate H).
    (* One subgoal left, which is where both are Step *)
    destruct (IHx p0).
    + destruct (string_dec i i0); subst.
      * auto.
      * right.
        intro H.
        contradiction n.
        injection H.
        tauto.
    + right.
      intro H.
      contradiction n.
      injection H.
      tauto.
  - (* Prove eq_dec for InitStep *)
    destruct y; try (right; intro H; discriminate H).
    (* One subgoal left, which is where both are InitStep *)
    destruct (string_dec i i0); subst.
    + auto.
    + right.
      intro H.
      contradiction n.
      injection H.
      tauto.
  - (* Prove eq_dec for Path *)
    intro.
    destruct p2.
    destruct (IHx l0); subst.
    + auto.
    + right.
      intro H.
      contradiction n.
      injection H.
      tauto.
  - (* Prove eq_dec for @nil STEP *)
    intro.
    destruct l2.
    + auto.
    + right.
      intro H.
      discriminate H.
  - (* Prove eq_dec for cons STEP *)
    intro..
    destruct l2.
    + right.
      intro H.
      discriminate H.
    + destruct (IHx s); subst.
      * destruct (IHx0 l2); subst.
        {
          auto.
        }
        {
          right.
          intro H.
          contradiction n.
          injection H.
          tauto.
        }
      * right.
        intro H.
        contradiction n.
        injection H.
        tauto.
Qed.

 

Best regards,

Frédéric.

but Coq says Error: Attempt to save an incomplete proofCompilation output:

Thanks in advance,
Saulo