blob: b48684ba88b2fd65a56234a59dc816e9a0679355 (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
Require Import NumPrelude.
Module Type DomainSignature.
Parameter Z : Set.
Parameter E : relation Z.
Parameter e : Z -> Z -> bool.
Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
Axiom E_equiv : equiv Z E.
Add Relation Z E
reflexivity proved by (proj1 E_equiv)
symmetry proved by (proj2 (proj2 E_equiv))
transitivity proved by (proj1 (proj2 E_equiv))
as E_rel.
Delimit Scope ZScope with Int.
Bind Scope ZScope with Z.
Notation "x == y" := (E x y) (at level 70) : ZScope.
Notation "x # y" := (~ E x y) (at level 70) : ZScope.
End DomainSignature.
Module DomainProperties (Export DomainModule : DomainSignature).
Open Local Scope ZScope.
Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
Proof.
intros x x' Exx' y y' Eyy'.
case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
assert (x == y); [rewrite Exx'; now rewrite Eyy' |
rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
Qed.
Theorem neq_symm : forall n m, n # m -> m # n.
Proof.
intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
Qed.
End DomainProperties.
|
