The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I redid the proofs at home, this gives:

******************************

Require Import String.

Definition ID := string.

Definition ID_dec := string_dec.

Inductive STEP : Type :=

  | LastStep : ID -> STEP

  | Step : ID -> PATH -> STEP

  | Init : ID -> STEP

with PATH : Type :=

  | EndOfPath : PATH

  | MorePaths : STEP -> PATH -> PATH.

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; (clear - _H0 _H || clear - _H || idtac);

abstract ((now subst)||(intro Heq; inversion Heq; auto)).

(*PATH_dec*)refine (

  match p1, p2 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; (clear - _H0 _H || clear - _H || idtac);

abstract ((now subst)||(intro Heq; inversion Heq; auto)).

Defined.

============================

But as I said earlier, this is only if you can accept to get rid of the 'list' type constructor.

2014-12-10 11:13 GMT+01:00 Cedric Auger <sedrikov AT gmail.com>:

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.