Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] decluttering proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] decluttering proofs


chronological Thread 
  • From: Adam Koprowski <adam.koprowski AT gmail.com>
  • To: Ian Lynagh <igloo AT earth.li>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] decluttering proofs
  • Date: Wed, 24 Feb 2010 00:54:43 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=W/uPKix904foT24SMOIx5/BWXrW0dZ8uc5b04vNoBeiiPbzddlpEQ/kFUZGueC8xWJ LivuqRskBVMOQDYFGXmUO3C4hua26OuwAo1moOVYCze225wtLL1+2x1a0ZfzdcjWwBh2 gAoEyBzcYt8Mt0Dm9PeWJDt24n/Rx+y4NkzHo=

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?
 
Ideally I'd like to get it to the point where
the statement is not much more verbose than
   ((x :> ys) :+> zs) = (x :> (ys :+> zs))
  I think you can greatly improve readability of your development by cleverly using implicit arguments and notations. In particular you will find the new mechanism for implicit quantification that comes with type-classes particularly useful (see Section 18.2.1 of the manual). Below find my quick go at defining append in a more concise way (starting with a replacement for your definition of Sequence). I think you should be able to continue in a similar fashion to obtain a version of myLemma closer to what you want.

   Good luck,
   Adam

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

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).

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]



Archive powered by MhonArc 2.6.16.

Top of Page