search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

destructing sumbools #85

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

Say I want to prove something like : (if eq_id_dec x x then n else st x) = n. What I'd like to do is prove some lemma like eq_id_dec = true. How can we do this with sumbools though? I know an alternative is to do destruct (eq_id_dec x x, but I get stuck on the case where x!=x so I'd like to avoid using destruct.

jeehoonkang commented 9 years ago

If you have H: x <> x, then exfalso; apply H; auto will solve the goal.

Jeehoon

jaewooklee93 commented 9 years ago

Thank you. I always used assert (x=x) and then drew contradiction. Your method is much simpler.

jeehoonkang commented 9 years ago

It would be also nice to state something like: Lemma eq_id_dec_true {A} x (a1 a2:A): (if eq_id_dec x x then a1 else a2) = a1.

AdamBJ commented 9 years ago

The first way worked for me, thanks Jeehoon.