SHARE
TWEET

Untitled

a guest Jul 30th, 2017 120 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (* Some small examples, because the method is exponential *)
  2.  
  3. Lemma exemple1 : forall a b, negb (orb a b) = andb (negb a) (negb b).
  4. intros. validity.
  5. Qed.
  6.  
  7. Lemma exemple2 : forall a b c,
  8. negb a || negb b || (c && true) = negb (a && b && negb c).
  9. intros. validity.
  10. Qed.
  11.  
  12. Lemma exemple3 : forall a,
  13. negb (negb a) = a.
  14. intros. validity.
  15. Qed.
  16.  
  17. Lemma exemple4 : forall a b, a && a && b = b && b && a.
  18. intros. validity.
  19. Qed.
  20.  
  21. Lemma exemple5 : forall a b c,
  22. (a && b) || (negb a && c) = (negb a || b) && (a || c).
  23. intros. validity.
  24. Qed.
  25.  
  26. (* This example fails because the identity is false *)
  27. Lemma false_ex1 : forall a b,
  28. a || b = negb a || negb b.
  29. intros. validity. admit.
  30. Qed.
  31.  
  32. (* This example fails because of the method can't see that
  33.   n1 >= n2 and n2 >= n1 are related *)
  34. Lemma false_ex2 : forall n1 n2 : nat,
  35. greater_eq n1 n2 || greater_eq n2 n1 = true.
  36. intros. validity. admit.
  37. Qed.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Top