search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Going from H : bequiv b b' to b = b' #110

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

I feel embarrassed to ask this, but I can't figure out how finish the proof below:

H : bequiv b b' __(1/1) b = b'

Can someone help me out?

jeehoonkang commented 9 years ago

Would you please give me the definition of bequiv?

Jeehoon

AdamBJ commented 9 years ago

Definition bequiv (b1 b2 : bexp) : Prop := forall (st:state), beval st b1 = beval st b2.

jaewooklee93 commented 9 years ago

I think it is impossible..

Equality is somewhat stronger notion than equivalence

Two expressions (BTrue) and (BNot BFalse) are just equivalent, which means they always return the same output whatever memory (state) is given, but they are not equal. For being equal to each other, each boolean expression must have exactly the same form.

The notion of equality is quite strict, so we cannot directly use that notion to solve our problem. In order to bypass this difficulty, we defined another notion, equivalence, which can be considered as a relaxed form of equality.

jaewooklee93 commented 9 years ago 
Theorem impossible:
  (forall b b', bequiv b b' -> b=b') -> False.
Proof.
  intros; assert (bequiv BTrue (BNot BFalse)).
  constructor.
  apply H in H0; inversion H0.
Qed.

If you really want to prove b=b', you have to bring a stronger evidence other than just equivalence.

AdamBJ commented 9 years ago

Ok, thanks @jaewooklee93!