The Coq mailing list

["Aaron B." <aaron678 AT gmail.com>]

Thanks.  I find the point in your last comment especially interesting.

 - Aaron

On Fri, Oct 22, 2010 at 9:20 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> 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.")
> *)
>
>