CODEWITHSUNDEEP
coq
acogrunge
acogrunge

Reputation: 13

false = true problem when solving Lemma in Coq

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?

Upvotes: 0

Views: 91

Answers (2)

acogrunge
acogrunge

Reputation: 13

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.

Upvotes: 0

Pierre Castéran
Pierre Castéran

Reputation: 916

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.

Upvotes: 1

Related Questions