coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ian Lynagh <igloo AT earth.li>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] C-zar proof help
- Date: Mon, 2 Mar 2009 23:21:36 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi all,
I'm very new to coq, and am trying to do some proofs with C-zar. I'm
currently largely stumbling in the dark, but I'm hoping that will
improve once I've got a proof or two done.
In the attached coq file I make an axiom:
(commute (p, q) = Some (q', p')
-> commute (q', p') = Some (p, q)).
for UnnamedPatch's, and then I try to prove
(namedCommute (p, q) = Some (q', p')
-> namedCommute (q', p') = Some (p, q)).
for NamedPatch's, where
Inductive NamedPatch : Set
:= MkNamedPatch : Name -> UnnamedPatch -> NamedPatch.
and namedCommute basically just does commute on the UnnamedPatch's. The
proof is incomplete, and the last line goes orange (but I don't really
understand why). Also, even if it was green, I'm not sure what would
come next. "thus thesis."?
Remnants of some other avenues I explored are in comments at the end.
I would be very grateful if anyone could shed any light. Suggestions for
any other ways to improve the proof, or completely different ways to
approach it, also welcome! Readability of the proof is very important to
me.
Thanks
Ian
Variable UnnamedPatch : Set.
Variable commute : (UnnamedPatch * UnnamedPatch)
-> option (UnnamedPatch * UnnamedPatch).
Axiom UnnamedPatchCommuteSelfInverse :
forall (p : UnnamedPatch)
(q : UnnamedPatch)
(p' : UnnamedPatch)
(q' : UnnamedPatch),
(commute (p, q) = Some (q', p')
-> commute (q', p') = Some (p, q)).
Variable Name : Set.
Inductive NamedPatch : Set
:= MkNamedPatch : Name -> UnnamedPatch -> NamedPatch.
Definition namedCommute (pq : NamedPatch * NamedPatch)
: option (NamedPatch * NamedPatch)
:= match pq with
(MkNamedPatch np p, MkNamedPatch nq q) =>
match commute (p, q) with
| Some (q', p') => Some (MkNamedPatch nq q', MkNamedPatch np p')
| None => None
end
end.
Lemma NamedPatchCommuteSelfInverse :
forall (p : NamedPatch)
(q : NamedPatch)
(p' : NamedPatch)
(q' : NamedPatch),
(namedCommute (p, q) = Some (q', p')
-> namedCommute (q', p') = Some (p, q)).
proof.
let p : NamedPatch,
q : NamedPatch,
p' : NamedPatch,
q' : NamedPatch
be such that (namedCommute (p, q) = Some (q', p')).
per cases on p.
suppose it is (MkNamedPatch np up).
per cases on q.
suppose it is (MkNamedPatch nq uq).
per cases on p'.
suppose it is (MkNamedPatch np' up').
per cases on q'.
suppose it is (MkNamedPatch nq' uq').
per cases on (commute (up, uq)).
suppose it is None.
(* claim (namedCommute (MkNamedPatch np up, MkNamedPatch nq uq) = None).
*)
have (namedCommute (MkNamedPatch np up, MkNamedPatch nq uq) =
match (MkNamedPatch np up, MkNamedPatch nq uq) with
(MkNamedPatch np up, MkNamedPatch nq uq) =>
match commute (up, uq) with
| Some (uq', up') => Some (MkNamedPatch nq uq', MkNamedPatch np
up')
| None => None
end
end).
~= (match commute (up, uq) with
| Some (uq', up') => Some (MkNamedPatch nq uq', MkNamedPatch np
up')
| None => None
end).
~= None.
(*
reconsider thesis as
((match (MkNamedPatch np up, MkNamedPatch nq uq) with
(MkNamedPatch np up, MkNamedPatch nq uq) =>
match commute (up, uq) with
| Some (uq', up') => Some (MkNamedPatch nq uq', MkNamedPatch np
up')
| None => None
end
end) = None).
reconsider thesis as
((match commute (up, uq) with
| Some (uq', up') => Some (MkNamedPatch nq uq', MkNamedPatch np
up')
| None => None
end) = None).
*)
(*
thus thesis by (commute (up, uq) = None).
end claim.
have (namedCommute (MkNamedPatch np up, MkNamedPatch nq uq) = None) by
namedCommute.
then (namedCommute (MkNamedPatch np up, MkNamedPatch nq uq) = None) by
namedCommute.
then (namedCommute (p, q) = None).
thus thesis.
end cases
*)
(*
then (commute (up, uq) = Some (uq', up')
-> commute (uq', up') = Some (up, uq)) by UnnamedPatchCommuteSelfInverse.
*)
(*
then (namedCommute (p, q) = Some (q', p')
-> namedCommute (q', p') = Some (p, q)).
then (commute (up, uq) = Some (uq', up')).
then (namedCommute (q', p') = Some (p, q)).
end proof.
*)
- [Coq-Club] C-zar proof help, Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Adam Chlipala
- Re: [Coq-Club] C-zar proof help,
Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Adam Chlipala
- Re: [Coq-Club] C-zar proof help, Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Adam Chlipala
- Re: [Coq-Club] C-zar proof help,
Ian Lynagh
- Re: [Coq-Club] C-zar proof help, Pierre Corbineau
- Re: [Coq-Club] C-zar proof help, Taral
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help, Ian Lynagh
- Re: [Coq-Club] C-zar proof help,
Taral
- Re: [Coq-Club] C-zar proof help,
Adam Chlipala
Archive powered by MhonArc 2.6.16.