• API
• FAQ
• Tools
• Archive
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.
Top