The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Dear Cedric Auger, Pierre-Yve, Kyle Stemen and Frédéric, 

Thanks a lot for yours suggestions and proofs. I am going to evaluate which one better fits to my very limited Coq knowledge. In any case, it is always good to know alternatives ways to do something. 

Saulo

On Wed, Dec 10, 2014 at 7:13 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

Do you heavily rely on functions on lists ?
If not, you could consider to rewrite your type as follows:

Inductive STEP : Type :=
  | LastStep : ID -> STEP
  | Step : ID -> PATH -> STEP
  | Init : ID -> STEP
with PATH : Type :=
  | EndOfPath : PATH
  | MorePaths : STEP -> PATH -> PATH.

That would remove some annoyance with external inductive type constructors (although they can still be dealt with as Kyle proved).

Then you could define something like:

Fixpoint STEP_dec (s1 s2 : STEP) : {s1=s2}+{s1<>s2}
with PATH_dec (p1 p2 : PATH) : {p1=p2}+{p1<>p2}.

(*STEP_dec*)refine (
  match s1, s2 with
  | LastStep x, LastStep y => if ID_dec x y then left _ _ else right _ _
  | Step x p1, Step y p2 => if ID_dec x y then if PATH_dec p1 p2 then left _ _ else right _ _ else right _ _
  | Init x, Init y => if ID_dec x y then left _ _ else right _ _
  | _, _ => right _ _
  end
); clear STEP_dec PATH_dec.
<do 13 easy proofs, the following tactics should be enough: reflexivity/split, subst/rewrite, discriminate/inversion/destruct.
 I often pack them in an "abstract(<tactic>)." to remove proofs from the final term after cleaning unneeded hypotheses >

(*PATH_dec*)refine (
  match s1, s2 with
  | EndOfPath, EndOfPath => left _ _
  | MorePaths s1 p1, MorePaths s2, p2 => if STEP_dec s1 s2 then if PATH_dec p1 p2 then left _ _ else right _ _ else right _ _
  | _, _ => right _ _
  end
); clear STEP_dec PATH_dec.
<do 6 easy proofs, the following tactics should be enough: reflexivity/split, subst/rewrite, discriminate/inversion/destruct.
 I often pack them in an "abstract(<tactic>)." to remove proofs from the final term after cleaning unneeded hypotheses >

Defined.

I did not tried it (cannot do it yet), so it may contain many errors.
One of them is on the name of the constructors of {_}+{_}. I used left and right, but I may be confused with inl and inr or in_left and in_right. I never remember which one builds which type. Then there is also the number of "_" after "left" and "right". I also assume that ID_dec is already defined.

2014-12-10 9:40 GMT+01:00 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