Skip to Content.
Sympa Menu

coq-club - [Coq-Club] decluttering proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] decluttering proofs


chronological Thread 
  • From: Ian Lynagh <igloo AT earth.li>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] decluttering proofs
  • Date: Tue, 23 Feb 2010 21:32:29 +0000


Hi all,

I have some proofs about sequences of things, where the sequence type
also contains proofs that it is well-formed. I've attached a simplified
version (explicit.v).

My main problem is that the code that handles maintaining these proofs
is cluttering up my coq code. For example, if you look at the definition
of append, or at the lemma myLemma, it's very unclear what's actually
going on.

Someone on IRC suggested that I use Program, and that helps (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. 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))


Is Program the best way to go? Someone else suggested to me a while ago
that I could use type classes to solve this problem, but I don't
understand how that would work? Or if Program is the best way forward,
what should myLemma look like?

Also, I have the impression that I should be using setoids somehow, so
that all my equalities are modulo set equality, but I don't know how to
do that. Any clues?


Any advice gratefully received!


Thanks
Ian


Module Export sequences.

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

(* ===== 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.

Inductive Sequence (from to : NameSet.t)
                   (contains : ThingSet.t)
                 : Type
    := Nil : forall (fromToOK : NameSet.Equal from to)
                    (containsOK : ThingSet.Equal contains ThingSet.empty),
             Sequence from to contains
     | Cons : forall {from' mid : NameSet.t}
                     {qsContains : ThingSet.t}
                     (p : Patch from' mid)
                     (qs : Sequence mid to qsContains)
                     (fromOK : NameSet.Equal from from')
                     (containsOK : ThingSet.Equal contains (ThingSet.add 
(thingOf p) qsContains)),
              Sequence from to contains.
Implicit Arguments Nil  [from to contains].
Implicit Arguments Cons [from to contains from' mid qsContains].
Notation "s :> t" := (Cons s t _ _)
    (at level 60, right associativity).
Notation "[]" := (Nil _ _)
    (no associativity).

(* ===== Lemmas ===== *)

Lemma appendLemma1 {x y z : ThingSet.t}
                   (proofX : ThingSet.Equal x ThingSet.empty)
                   (proofY : ThingSet.Equal y ThingSet.empty)
                   (proofZ : ThingSet.Equal z (ThingSet.union x y))
                    : ThingSet.Equal z ThingSet.empty.
intros.
fsetdec.
Qed.

Lemma appendLemma2 {n : Thing}
                   {x x' y z : ThingSet.t}
                 : ThingSet.Equal x (ThingSet.add n x')
                -> ThingSet.Equal y ThingSet.empty
                -> ThingSet.Equal z (ThingSet.union y x)
                -> ThingSet.Equal z (ThingSet.add n x').
Proof.
intros.
fsetdec.
Qed.

Lemma appendLemma3 {n : Thing}
                   {x x' y z : ThingSet.t}
                 : ThingSet.Equal x (ThingSet.add n x')
                -> ThingSet.Equal z (ThingSet.union x y)
                -> ThingSet.Equal z (ThingSet.add n (ThingSet.union x' y)).
Proof.
intros.
fsetdec.
Qed.

(* ===== Append ===== *)

Fixpoint append {from mid to : NameSet.t}
                {psContains qsContains psQsContains : ThingSet.t}
                (containsOK : ThingSet.Equal
                                  psQsContains
                                  (ThingSet.union psContains qsContains))
                (ps : Sequence from mid psContains)
                (qs : Sequence mid to qsContains)
       : Sequence from to psQsContains
    := match ps with
       | Nil psFromToOK psContainsOK =>
               match qs with
               | Nil qsFromToOK qsContainsOK =>
                   Nil (NameSet.eq_trans psFromToOK qsFromToOK)
                       (appendLemma1 psContainsOK qsContainsOK containsOK)
               | Cons from' mid' qs'Contains q qs' qsFromOK qsContainsOK =>
                   Cons q
                        qs'
                        (NameSet.eq_trans psFromToOK qsFromOK)
                        (appendLemma2 qsContainsOK psContainsOK containsOK)
               end
       | Cons from' mid' ps'Contains p ps' psFromOK psContainsOK =>
               Cons p
                    (append (ThingSet.eq_refl _) ps' qs)
                    psFromOK
                    (appendLemma3 psContainsOK containsOK)
       end.
Notation "ps :+> qs" := (append _ ps qs)
    (at level 60, right associativity).

Lemma helper {x : Thing}
             {y z xy xyz : ThingSet.t}
             (H1 : ThingSet.Equal xyz (ThingSet.add x (ThingSet.union y z)))
             (H2 : ThingSet.Equal xy (ThingSet.add x y))
           : ThingSet.Equal xyz (ThingSet.union xy z).
intros.
ThingSetDec.fsetdec.
Qed.

Theorem myLemma {o ox oxy oxyz : NameSet.t}
                {ysContains zsContains xYsContains xYsZsContains : ThingSet.t}
                (x : Patch o ox)
                (ys : Sequence ox oxy ysContains)
                (zs : Sequence oxy oxyz zsContains)
                (xYsContainsOK : ThingSet.Equal xYsContains (ThingSet.add 
(thingOf x) ysContains))
                (xYsZsContainsOK : ThingSet.Equal xYsZsContains (ThingSet.add 
(thingOf x) (ThingSet.union ysContains zsContains)))
              : (append (helper xYsZsContainsOK xYsContainsOK)
                        (Cons x ys (NameSet.eq_refl _) xYsContainsOK)
                        zs)
                =
                (Cons x
                      (append (ThingSet.eq_refl _)
                              ys
                              zs)
                      (NameSet.eq_refl _)
                      xYsZsContainsOK).
Proof.
intros.
unfold append at 1.
fold (append (ThingSet.eq_refl (ThingSet.union ysContains zsContains)) ys zs).
f_equal.
apply proof_irrelevance.
Qed.

End sequences.

Module Export sequences.

Require Export FSets.
Require Export FSetDecide.
Require Export FSetProperties.
Require Import FSetWeakList.
Require Import ProofIrrelevance.
Require Import 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.

Inductive Sequence (from to : NameSet.t)
                   (contains : ThingSet.t)
                 : Type
    := Nil : forall (fromToOK : NameSet.Equal from to)
                    (containsOK : ThingSet.Equal contains ThingSet.empty),
             Sequence from to contains
     | Cons : forall {from' mid : NameSet.t}
                     {qsContains : ThingSet.t}
                     (p : Patch from' mid)
                     (qs : Sequence mid to qsContains)
                     (fromOK : NameSet.Equal from from')
                     (containsOK : ThingSet.Equal contains (ThingSet.add 
(thingOf p) qsContains)),
              Sequence from to contains.
Implicit Arguments Nil  [from to contains].
Implicit Arguments Cons [from to contains from' mid qsContains].
Notation "s :> t" := (Cons s t _ _)
    (at level 60, right associativity).
Notation "[]" := (Nil _ _)
    (no associativity).

(* ===== Append ===== *)

Program Fixpoint append
                {from mid to : NameSet.t}
                {psContains qsContains psQsContains : ThingSet.t}
                (containsOK : ThingSet.Equal
                                  psQsContains
                                  (ThingSet.union psContains qsContains))
                (ps : Sequence from mid psContains)
                (qs : Sequence mid to qsContains)
       : Sequence from to psQsContains
    := match ps with
       | Nil _ _ =>
               match qs with
               | Nil _ _ =>
                   []
               | Cons _ _ _ q qs' _ _ =>
                   q :> qs'
               end
       | Cons _ _ _ p ps' _ _ =>
               p :> (append (ThingSet.eq_refl _) ps' qs)
       end.
Next Obligation.
NameSetDec.fsetdec.
Qed.
Next Obligation.
ThingSetDec.fsetdec.
Qed.
Next Obligation.
NameSetDec.fsetdec.
Qed.
Next Obligation.
ThingSetDec.fsetdec.
Qed.
Next Obligation.
ThingSetDec.fsetdec.
Qed.
Notation "ps :+> qs" := (append _ ps qs)
    (at level 60, right associativity).

Lemma helper {x : Thing}
             {y z xy xyz : ThingSet.t}
             (H1 : ThingSet.Equal xyz (ThingSet.add x (ThingSet.union y z)))
             (H2 : ThingSet.Equal xy (ThingSet.add x y))
           : ThingSet.Equal xyz (ThingSet.union xy z).
intros.
ThingSetDec.fsetdec.
Qed.

Program Theorem myLemma
                {o ox oxy oxyz : NameSet.t}
                {ysContains zsContains xYsContains xYsZsContains : ThingSet.t}
                (x : Patch o ox)
                (ys : Sequence ox oxy ysContains)
                (zs : Sequence oxy oxyz zsContains)
                (xYsContainsOK : ThingSet.Equal xYsContains (ThingSet.add 
(thingOf x) ysContains))
                (xYsZsContainsOK : ThingSet.Equal xYsZsContains (ThingSet.add 
(thingOf x) (ThingSet.union ysContains zsContains)))
              : (append (helper xYsZsContainsOK xYsContainsOK)
                        (Cons x ys _ xYsContainsOK : Sequence o oxy 
xYsContains)
                        zs)
                =
                (Cons x
                      (append (ThingSet.eq_refl _)
                              ys
                              zs)
                      (NameSet.eq_refl _)
                      xYsZsContainsOK).
Proof.
intros.
unfold append at 1.
fold (append (ThingSet.eq_refl (ThingSet.union ysContains zsContains)) ys zs).
f_equal.
apply proof_irrelevance.
Qed.

End sequences.



Archive powered by MhonArc 2.6.16.

Top of Page