The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

I am trying to write a proof that inverting something twice is the
identity. I have a proof (thingInverseInverseDestructingSign in the
attached script), but it involves destructing Sign, which feels
unsatisfactory to me.

I would prefer a way to prove it that doesn't depend on the
implementation of Sign. The problem is that the two things I am trying
to prove the equality of are of this type:

    Record Thing (from to : natSet) : Type := mkThing {
        th_me : SignedNat;
        th_natOK : natOK from to th_me
    }.

so if the th_me's have a different value, then f_equal does nothing as
the types of the th_natOK's are different.

"apply proof_irrelevance." believes that it can prove it, but Qed
disagrees (probably another instance of bug #2240) (thingInverseInverse
in the attached script).

Is there a way to complete this proof without destructing the Sign?


Thanks
Ian


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

(* BEGIN: make a "Set of nat" type *)
Module DecidableNat.
Definition t := nat.
Definition eq := @eq nat.
Definition eq_refl := @refl_equal nat.
Definition eq_sym := @sym_eq nat.
Definition eq_trans := @trans_eq nat.
Definition eq_dec := eq_nat_dec.
End DecidableNat.

Module natSetMod := Make(DecidableNat).

Notation natSet := (natSetMod.t).
Notation natSetIn := (natSetMod.In).
Notation natSetAdd := (natSetMod.add).
Notation natSetEqual := (natSetMod.Equal).
(* END: make a "Set of nat" type *)

Inductive Sign : Set
    := Positive | Negative.

Inductive SignedNat : Set
    := MkSignedNat : forall (s : Sign)
                            (n : nat),
                     SignedNat.

Definition signedNatInverse (n : SignedNat) : SignedNat
    := match n with
       | MkSignedNat Positive b => MkSignedNat Negative b
       | MkSignedNat Negative b => MkSignedNat Positive b
       end.

Lemma signedNatInverseInverse : forall (sn : SignedNat), signedNatInverse 
(signedNatInverse sn) = sn.
Proof with auto.
intros.
destruct sn.
destruct s...
Qed.

Definition natOK (from to : natSet)
                 (sn : SignedNat)
               : Prop
    := match sn with
       | MkSignedNat Positive n => (~ natSetIn n from)
                                /\ (natSetEqual to (natSetAdd n from))
       | MkSignedNat Negative n => (~ natSetIn n to)
                                /\ (natSetEqual from (natSetAdd n to))
       end.

Record Thing (from to : natSet) : Type := mkThing {
    th_me : SignedNat;
    th_natOK : natOK from to th_me
}.
Implicit Arguments mkThing [from to].
Implicit Arguments th_me [from to].
Implicit Arguments th_natOK [from to].

Lemma natOKInverse : forall {from to : natSet}
                            {n : SignedNat}
                            (ok : natOK from to n),
                     natOK to from (signedNatInverse n).
Proof with auto.
intros.
destruct n.
destruct s.
    simpl.
    destruct ok.
    split...
simpl.
destruct ok.
split...
Qed.

Definition thingInverse {from to : natSet}
                        (thing : Thing from to)
                      : Thing to from
 := mkThing (signedNatInverse (th_me thing))
            (natOKInverse (th_natOK thing)).

Lemma thingInverseInverseDestructingSign :
      forall {from to : natSet}
             (p : Thing from to),
      thingInverse (thingInverse p) = p.
Proof with auto.
intros.
destruct p.
unfold thingInverse.
simpl.
destruct th_me0.
destruct s.
    simpl.
    f_equal.
    apply proof_irrelevance.
simpl.
f_equal.
apply proof_irrelevance.
Qed.

Lemma thingInverseInverse :
      forall {from to : natSet}
             (p : Thing from to),
      thingInverse (thingInverse p) = p.
Proof with auto.
intros.
destruct p.
unfold thingInverse.
simpl.

(* Now want to be able to say: *)
f_equal.
(* but it does nothing, as the types don't match *)

(* We /are/ able to apply proof irrelevance: *)
apply proof_irrelevance.
(* But then Qed fails with a type error: *)
Qed.