The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

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