0

I have definition:

Definition f (b1 b2 : bool) :bool := 
match b1 with  
| true => true
| false => b2
end.

And Lemma...

Lemma l1: forall p : bool, f p false = true.

What I have tried is this:

Lemma l1: forall p : bool, f p false = true.
Proof.
intros p.
destruct p.
simpl.
reflexivity.
simpl.

And then I get false=true. What to do?

2 Answers 2

1

You cannot prove l1, since f false false = false.

Perhaps you would like to prove:

Lemma l1: forall p : bool, f p false = p.

instead.

0

Actually the definition was n ot good. Here it is.

Definition f (b1 b2 : bool) : bool := 
  match b1, b2 with  
  | false, true => false
  | _, _ => true
  end.

And then I did proof in this way. Am I right?

Lemma l1: forall p : bool, f p false = true.
Proof.
intros p.
destruct p.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
1
  • Your proof is correct. Using tacticals, you can make the proof script shorter and more readable: Proof. destruct p; reflexivity. Qed.. Please note that it's important not to build proofs about erroneous definitions ... Aug 30 at 17:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.