On Thu, Apr 16, 2009 at 04:11:32PM +0200, Florent Becker wrote:
> Ian Lynagh <[email protected]> writes:
>
> > Yes, I don't object to using states. The only reason I haven't is to
> > keep it simpler for now.
> >
> Ok, my experience is that when doing the actual (coq or manual )proofs,
> states are more a help than anhindrance. So we should go for them.
I still have contexts (sets of names) on named patches, so it's only
the simple, lowest-level proofs that don't have them.
> >> 4/ Unnamed marked sequences
> >>
> >> before introducing names (they don't exist yet in dic), dic relies on a
> >> concept which is not present in camp-paper, nor in camp-coq.
> >>
> >> That concept is that of marked sequences (shuffle_mark_[1,2] in
> >> dic). The idea is that if s (with p marked) can be shuffled into t (with q
> >> marked),
> >> then when shuffling s into t, p "lands" on q. (There is also a version with
> >> two marks). Additionally, one will need a lossy version, with
> >> s (with p marked) can be turned into t (with q marked) if by shuffling
> >> patches in s, adding and removing patches, p "lands" on q.
> >
> > This feels like an ugly kludge to me. The "obvious" human proofs for
> > some of the lemmas required a similar kludge, but I managed to find a
> > way to do the proofs that didn't need it in the end. I hope we can avoid
> > it with machine proofs too.
> >
> What lemmas and what proofs are concerned by this? How did you get out of
> that situation? I want to know, because i don't find it is a kludge, and i
> don't see
> any other way to _completely_ do some proofs.
The troublesome one was proving that if
as p q bs <->* cs p' q' ds
then p and q commute iff p' and q' do.
In the end I proved it by showing that if as = a:as' then at each step
of the <->* you can directly commute "a" to the left without affecting
the truth of the result. Therefore if it's false for any sequence, it's
false for a sequence with as = []. Likewise bs = []. And it's trivially
true for as = bs = []. Contradiction, so it is true for all sequences.
(assuming each patch's name is unique).
> So not all sequences are straight, but there
> are some places where sequences that arise are guaranteed to be straight. Is
> that right?
Yes.
> >> 6/ names as a function or a component of patches
> >>
> >> Second, Ian's proofs that 'c' holds are difficult
> >
> > We've talked about this OOB, and I think we're agreed that we need to be
> > able to do these proofs, because they're simpler versions of the catch
> > proofs that we're going to have to do.
> >
> > I still think that my way, i.e. constructing named patches from unnamed
> > patches and names, is the best way. But even if I didn't, I think that
> > doing these simple proofs will help me understand how best to write the
> > big proofs, so I plan to continue with this.
>
> Ok, i agree with the training bit, even though i'm not sure those proofs are
> actually much simpler than the catch proofs, since they require setoid
> manipulations for the namesets.
Maybe "smaller" is a better word than "simpler".
> will be not that much more to build, since they are only _sequences_ of names
> there, no fsets.
Well, there is a set of conflicts, but you could probably represent that
as a list.
> > Then the patch universe says: Given a patch type P, and lemmas L1 and L2
> > on P, there is a patch universe in which L3, L4, L5 are true.
> ok
> >
> > Roughly speaking, L1 and L2 are how triples of patches are related by
> > commutation, and L3+ are things like "patches in a sequence (or, indeed,
> > theentire universe) have a minimal context".
> So why not make L3 be "patches have a minimal context?" That's what I'm
> advocating (actually something a bit weaker: that they have a common
> straight context).
L3 is that. But L3 is proven by L1 and L2.
> > So the point of patch universes is that we don't have to prove that
> > named patches /and/ catches have minimal context, we only have to prove
> > that patch-like things have minimal context.
> >
> Note that by N1 and N2, and C1 and C2, this is the case whichever
> formalisation for L3+ you take. So this argument is moot, since
> named patches and catches are /just a particular case of unnamed
> patches/.
I think we're on different wavelengths. I'm confused.
> >> My proposal is to end the madness. I propose to add an axiom that says
> >> that we can decide whether two patches are related, and draw the
> >> consequences.
> >
> > I don't want to add axioms about named patches. Apart from anything
> > else, if you need to make it an axiom for named patches then I can't see
> > how you're going to do it for catches. Or to phrase it differently: If
> > you can prove it for catches, I'm sure you could prove it for named
> > patches, so it has no business being an axiom.
>
> There's a fundamental misunderstanding here: i'm not adding as an axiom
> something you can prove. I'm advocating transforming one of your axioms.
>
> You had an axiom that says that record produces fresh names.
Well, I say that record takes a name that is fresh, yes.
record says that if you have
(u :: Patch)
(repos@(repo : _) :: PatchUniverse)
(name u `notIn` names repos)
then
((u : repo) : repos)
is a PatchUniverse.
(using Haskell syntax, and being a bit lax with the details).
> if you doubt it really removes one axiom, the one it removes is the infinity
> of the set of names.
I don't require that there are infinitely many names, but if you run out
then you won't be able to record patches.
Thanks
Ian
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
