blob: 3473d082506efd78355e8787401187bf7dbdc8be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
Require Import SMTCoq.
Require Import Bool.
Local Open Scope int63_scope.
Parameter f : Z -> Z.
Lemma sym_zeq_bool x y :
Zeq_bool x y = Zeq_bool y x.
Proof.
case_eq (Zeq_bool x y).
rewrite <- Zeq_is_eq_bool. intro H. symmetry. now rewrite <- Zeq_is_eq_bool.
symmetry. apply not_true_is_false.
intro H1. rewrite <- Zeq_is_eq_bool in H1.
symmetry in H1. rewrite Zeq_is_eq_bool in H1.
rewrite H in H1. discriminate H1.
Qed.
Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0).
Lemma f_1 : f 1 =? 1.
Proof.
verit_base f_spec; vauto; rewrite Z.eqb_sym; auto.
Qed.
|
