The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

eheh, thank you both for your solutions posted so quickly.

Stay cool!

2012/11/7 gallais <guillaume.allais AT ens-lyon.org>

Hi, If you don't care about names and don't mind a quick and dirty solution,

you can use something like this:

======================

Require Import Bool.

Lemma and_bool_inv : forall a b, a && b = true -> a = true /\ b = true.

Proof.

intros [] [] ; auto.

Qed.

Ltac split_my_ands := match goal with

  | H : ?a && ?b = true |- _ =>

   let myH := fresh "H" in

   assert (myH := and_bool_inv _ _ H) ; destruct myH ; clear H

end.

Goal forall a b c, a && b && c && (a && b) = true -> a = true /\ b = true.

intros ; repeat split_my_ands.

======================

Cheers,

--
gallais

On 7 November 2012 16:12, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Hello.

Let's say that you have an hypothesis of this shape

H: A /\ B /\ ... /\ C

you could do 

destruct H as (Ha, (..., Hc)...).

Now, lets consider this hypothesis instead

H: A && B && ... && C = true

So, is there a tactic (or a general approach ...) that could allow me to easily obtain something like

Ha: A = true

...

Hc: C = true

?

Cheers!

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.