Practico 4. Ej 8 parte 2

Practico 4. Ej 8 parte 2

de Pablo Daniel Martinez Arevalo -
Número de respuestas: 1

(* 2. LAnd : forall a b : bool, And a b = true <-> a = true /\ b = true *)

Lemma LAnd : forall a b : bool, And a b = true <-> a = true /\ b = true.

Proof.

intros.

unfold iff.

split.

intros.

split.

Llego hasta aquí y me tranco...como abro el And de la hipotesis H?


En respuesta a Pablo Daniel Martinez Arevalo

Re: Practico 4. Ej 8 parte 2

de Carlos Luna -

Hola.

Para poder usar la información de H deberías hacer análisis de casos en la/s variable/s booleanas que aparecen en el And; de lo contrario no vas a poder usar la información del And, que se define sobre valores true / false.

Quizás te convenga iniciar la prueba usando "case". Al tener el And instanciado podés usar simpl.

Saludos, Carlos