The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Wed, Feb 24, 2010 at 12:54:43AM +0100, Adam Koprowski wrote:
> >
> > Someone on IRC suggested that I use Program, and that helps
> 
>    Yes, though you are mainly using Program to strategically place holes (_)
> to be inferred by Coq/proven by you as extra obligations. Note that you
> could get the same effect without Program, by using refine (in general
> Program is much easier to work with, the only disadvantage I'm aware of is
> the fact that it places explicit coercions throughout the final term, which
> may make the reduction behavior of your definition somewhat more tricky to
> work with).
> 
> (e.g. you can actually see what append does in the attached Program.v),
> > although
> > the minimally altered statement of myLemma causes:
> >    Error: The statement obligations could not be resolved
> >    automatically, write a statement definition first.
> > which means little to me.
> 
>   How do you alert the lemma to get this message?

I've taken the file you sent, and added the lemma to it. I can now get
the statement down to just

    : ((x :> ys) :+> zs)
    = ((@cast _ _ _ (x :> (ys :+> zs)) _ H)).

which is a lot better (although I'm not entirely sure where the
improvement comes from; perhaps the key difference is that append now
returns something with a union type directly, rather than a type and a
proof that that type is equal to the union), although ideally I'd like
to get to

    : ((x :> ys) :+> zs)
    = |: (x :> (ys :+> zs)) :| .

but changing the H to an _ gives the above error.

I'm also still wondering if I should have something like

    :   ((x :> ys) :+> zs)
    === (x :> (ys :+> zs)) .

where === is some setoid equality operator.

I've attached my current code.


Thanks
Ian


Module Export sequences.

Require Export FSets.
Require Export FSetDecide.
Require Export FSetProperties.
Require Import FSetWeakList.
Require Import ProofIrrelevance.

Require Import Coq.Program.Program.

(* ===== Names ===== *)

Parameter Name : Set.
Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}.

Module DecidableName.
Definition t := Name.
Definition eq := @eq Name.
Definition eq_refl := @refl_equal Name.
Definition eq_sym := @sym_eq Name.
Definition eq_trans := @trans_eq Name.
Definition eq_dec := eq_Name_dec.
End DecidableName.

Module NameSet := Make(DecidableName).
Module Export NameSetDec := WDecide (NameSet).

(* ===== Things ===== *)

Parameter Thing : Set.
Axiom eq_Thing_dec : forall (n : Thing) (o : Thing), {n = o} + {n <> o}.

Module DecidableThing.
Definition t := Thing.
Definition eq := @eq Thing.
Definition eq_refl := @refl_equal Thing.
Definition eq_sym := @sym_eq Thing.
Definition eq_trans := @trans_eq Thing.
Definition eq_dec := eq_Thing_dec.
End DecidableThing.

Module ThingSet := Make(DecidableThing).
Module Export ThingSetDec := WDecide (ThingSet).

(* ===== Sequences ===== *)

Parameter Patch : NameSet.t -> NameSet.t -> Set.
Parameter thingOf : forall {from to : NameSet.t}, Patch from to -> Thing.

(* ===== The next bit is more-or-less what Adam Koprowski wrote ===== *)

Infix "[=]" := ThingSet.Equal (at level 40).
Infix "[U]" := ThingSet.union (at level 40).

Generalizable All Variables.

Reserved Notation "s --[ c ]-> t" (at level 40).
Inductive Sequence : forall (from to : NameSet.t) (contains : ThingSet.t),
Type :=
  | Nil : forall `{t : NameSet.t, e [=] ThingSet.empty},
          t --[e]-> t
  | Cons : forall `{p : Patch from mid,
                    s : Sequence mid to contains,
                    e [=] (ThingSet.add (thingOf p) contains)},
           from --[e]-> to
where "s --[ c ]-> t ":= (Sequence s t c).

Implicit Arguments Cons [from mid to contains e H].

Notation "s :> t" := (@Cons _ _ s _ _ t _ _) (at level 60, right
associativity).
Notation "[]" := (Nil) (no associativity).

Ltac setdec := auto; ThingSetDec.fsetdec || NameSetDec.fsetdec.

Lemma cast `{ps : from --[psc]-> to, psc [=] psc'} : from --[psc']-> to.
Proof.
  induction 1; intros.
  constructor; setdec.
  constructor 2 with (mid:=mid)(p:=p)(contains:=contains); setdec.
Qed.
Notation "|: s :|" := (@cast _ _ _ s _ _).

Obligation Tactic := program_simpl; try ThingSetDec.fsetdec || 
NameSetDec.fsetdec.
Reserved Notation "s :+> t" (at level 40).
Program Fixpoint append mid `{ps : from --[psc]-> mid}
                            `{qs : mid --[qsc]-> to}
                          : from --[psc [U] qsc]-> to :=
  match ps with
  | Nil _ _ _ => |: qs :|
  | Cons _ _ p _ _ ps' _ _ => p :> (ps' :+> qs)
  end
where "s :+> t" := (@append _ _ _ s _ _ t).
Implicit Arguments append [from mid to psc qsc].

(* ===== Now here's the lemma stated completely explicitly ===== *)

Theorem myLemma {o ox oxy oxyz : NameSet.t}
                {ysContains zsContains xYsContains ysZsContains xYsZsContains 
: ThingSet.t}
                (x : Patch o ox)
                (ys : Sequence ox oxy ysContains)
                (zs : Sequence oxy oxyz zsContains)
                (xYsContainsOK : xYsContains [=] (ThingSet.add (thingOf x) 
ysContains))
                (xYsZsContainsOK : xYsZsContains [=] (ThingSet.add (thingOf 
x) (ThingSet.union ysContains zsContains)))
                (H : xYsZsContains [=] (xYsContains [U] zsContains))
              : (@append oxy o xYsContains
                        (@Cons o ox x oxy ysContains ys xYsContains 
xYsContainsOK)
                        oxyz zsContains zs)
              = @cast o oxyz xYsZsContains
                    (@Cons o ox x oxyz (ysContains [U] zsContains)
                           (@append oxy ox ysContains ys oxyz zsContains zs)
                           xYsZsContains xYsZsContainsOK)
                    (xYsContains [U] zsContains) H.
Proof.
intros.
unfold append at 1.
program_simpl.
fold append.
apply proof_irrelevance.
(* We can't Qed this: 
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2240 *)
Admitted.

(* ===== The same lemma, mostly implicit: ===== *)

Program Theorem myLemma2
               `(x : Patch o ox)
               `(ys : Sequence ox oxy ysContains)
               `(zs : Sequence oxy oxyz zsContains)
               `(H : xYsZsContains [=] (xYsContains [U] zsContains))
               `(xYsContainsOK : xYsContains [=] (ThingSet.add (thingOf x) 
ysContains))
              : ((x :> ys) :+> zs)
              = ((@cast _ _ _ (x :> (ys :+> zs)) _ H)).
Proof.
intros.
unfold append at 1.
program_simpl.
fold append.
apply proof_irrelevance.
(* We can't Qed this: 
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2240 *)
Admitted.

(* ===== But if we change the H to an _ then it fails: ===== *)
(*
Error: The statement obligations could not be resolved automatically, 
write a statement definition first.
*)

Program Theorem myLemma3
               `(x : Patch o ox)
               `(ys : Sequence ox oxy ysContains)
               `(zs : Sequence oxy oxyz zsContains)
               `(H : xYsZsContains [=] (xYsContains [U] zsContains))
               `(xYsContainsOK : xYsContains [=] (ThingSet.add (thingOf x) 
ysContains))
              : ((x :> ys) :+> zs)
              = ((@cast _ _ _ (x :> (ys :+> zs)) _ _)).
Proof.
intros.
unfold append at 1.
program_simpl.
fold append.
apply proof_irrelevance.
Admitted.