The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 21 Oct 2010 21:40:06 +0000,
Adam Megacz 
<megacz AT cs.berkeley.edu>
 a écrit :

> 
> Aaron Bohannon 
>Â <bohannon AT cis.upenn.edu>
>  writes:
> > It seems like something must be wrong here.  Is there something I
> > should be using instead of "inversion H; congruence"?
> 
> If "destruct H" gives you the hypotheses you need (it doesn't always),
> you might try using it instead of inversion.  At least for me it
> speeds things up dramatically.
> 
>   - a
> 

In my experience, "destruct H." is always better as "inversion H."
when the dependent parameters of H are all simple variables.

>>>>
(* first simple comparison between destruct and inversion *)
Lemma false_is_not_true_1: false = true -> False.
Proof.
 intro H; inversion H.
 (* I know "discriminate." works, but it simply
    do what I wrote and is almost as long as
    what I have written *)
Qed.
Print false_is_not_true_1.
(*
false_is_not_true_1 = 
fun H : false = true =>
let H0 :=
  match H in (_ = y) return (y = true -> False) with
  | refl_equal =>
      fun H0 : false = true =>
      let H1 :=
        eq_ind false (fun e : bool => if e then False else True) I true
H0 in False_ind False H1
  end in
H0 (refl_equal true)
     : false = true -> False
*)
(* honestly, it is really painfull for me to read it *)

Lemma false_is_not_true_2: false = true -> False.
Proof.
 assert (CorruptedTrue := I: if true then True else False).
 intro H; destruct H.
 (* now all occurences of "true" are replaced by "false",
    'corrupting' "CorruptedTrue" *)
 exact CorruptedTrue.
Qed.
Print false_is_not_true_2.
(*
false_is_not_true_2 = 
let CorruptedTrue := I in
fun H : false = true =>
let b := true in
match H in (_ = y) return ((if y then True else False) -> False) with
| refl_equal => fun CorruptedTrue0 : False => CorruptedTrue0
end CorruptedTrue
     : false = true -> False
*)
(* I do not pretend it is easy to read, but at least the term
   has not so much pollution in it *)

(* Of course, we need to manually assert a
   "match [destructed dependent parameters] with
    | [possible cases for the destructed dependent parameters] => True
    | [impossible cases for the destructed dependent parameters] =>
False end",
    that is mainly what the inversion tactic automatically does with
    "fun e : bool => if e then False else True",
    and after having used our pattern matching, eliminate manually
    absurd cases using our assertion;
    once again, inversion does it automatically *)

(* Here is another example *)

(* some dummy inductive for our examples *)
Inductive Eq_bool: bool -> bool -> Prop :=
| Eq_true: Eq_bool true true
| Eq_false: Eq_bool false false.

(* a not very interesting lemma *)
Lemma X: forall b, Eq_bool b true -> ~false = b.
Proof.
 intros.
 (*inversion seems smart as only the 1st case of the inductive is
considered*) inversion H.
 exact false_is_not_true_2.
Qed.

Print X.
(*
X = 
fun (b : bool) (H : Eq_bool b true) =>
let H0 :=
  match H in (Eq_bool b0 b1) return (b0 = b -> b1 = true -> false <> b)
with | Eq_true =>
      fun (H0 : true = b) (H1 : true = true) =>
      eq_ind true (fun b0 : bool => true = true -> false <> b0)
        (fun _ : true = true => false_is_not_true_2) b H0 H1
  | Eq_false =>
      fun (H0 : false = b) (H1 : false = true) =>
      eq_ind false (fun b0 : bool => false = true -> false <> b0)
        (fun H2 : false = true =>
         let H3 :=
           eq_ind false (fun e : bool => if e then False else True) I
true H2 in False_ind (false <> false) H3) b H0 H1
  end in
H0 (refl_equal b) (refl_equal true)
     : forall b : bool, Eq_bool b true -> false <> b
*)
(* the proof is all but readable *)

Lemma Y: forall b, Eq_bool b true -> ~false = b.
Proof.
 intros.
 (*this example runs using destruct,
   for that, we need to have only variables as dependent parameters *)
 remember true as c.
 (*as "destruct H" will replace all occurences of "b" and "c" with
   first "true" (we'll have to prove "false<>true")
   then "false" (we'll have "Heqc: false=true"),
   that will be OK*)
 destruct H.
  exact false_is_not_true_2.
 now intros _; exact (false_is_not_true_2 Heqc).
 (* we also could have used "destruct (false_is_not_true2 Heqc).",
    but the proof term would have been less readable,
    because of a need to perform type-casting from False with
    "match H return false<>false with end" *)
Qed.

Print Y.
(*
Y = 
fun (b : bool) (H : Eq_bool b true) =>
let c := true in
let Heqc := refl_equal c in
match H in (Eq_bool b0 b1) return (b1 = true -> false <> b0) with
| Eq_true => fun _ : true = true => false_is_not_true_2
| Eq_false =>
    fun (Heqc0 : false = true) (_ : false = false) =>
    false_is_not_true_2 Heqc0
end Heqc
     : forall b : bool, Eq_bool b true -> false <> b
*)

(* like above, we need an assertion "c = true" to keep trace
   of modification of the value of "c" in the inductive type
*)
Goal forall b, Eq_bool b true -> ~false = b.
 intros.
 destruct H.
  intro; discriminate.
 intro.
 (* hard to prove now... *)
Abort.

(* so, as long as dependent parameters of inductives are simple
   variables, we don't have to keep trace of their value, and
   we can use "destruct" directly instead of "inversion",
   without making proof scripts longer.

   That is a reason why I prefer to have
   "f a = b" in my hypothesis than "b = f a";
   in the first case, the dependent parameter is "b", which is
    a simple variable and can be harmlessly replaced everywhere by
    "f a" with a destruct;
   in the second case, the dependent parameter is "f a",
    "destruct" will replace all occurences of "f a" with "b",
    losing the link between "f a" and "b";
    so if somewhere you have an occurence of "g a", or simply "a",
    then you can lose the possibility to prove your lemma.
   Of course I know the "rewrite" tactic, but this tactic is
   mainly an "inversion", so it produces unnecessarily big and
   hardly readable terms; the worst being "rewrite <- H.", which
   can always be directly replaced by "destruct H.", as far as I know.
   (I belive "rewrite <- H." performs a "symmetry in H; rewrite H.")
*)