verilog finite_ordinal.v
finite_ordinal.v
Set Printing Coercions.
Require Import Omega.
Inductive hoge (n:nat) : Type :=
| fuga (m:nat) : m < n -> hoge n.
Coercion nat_of_hoge {n:nat} (h : hoge n) :=
match h with
| fuga _ n _ => n
end.
Lemma _0_2 : 0 < 2. Proof. omega. Qed.
Lemma _1_2 : 1 < 2. Proof. omega. Qed.
Lemma _0_3 : 0 < 3. Proof. omega. Qed.
Lemma _1_3 : 1 < 3. Proof. omega. Qed.
Lemma _2_3 : 2 < 3. Proof. omega. Qed.
Check fuga 3 0 _0_3.
(* fuga 3 0 _0_3 *)
(* : hoge 3 *)
Check fuga 3 1 _1_3.
(* fuga 3 1 _1_3 *)
(* : hoge 3 *)
Check fuga 3 2 _2_3.
(* fuga 3 2 _2_3 *)
(* : hoge 3 *)
Definition f2_1 := fuga 2 1 _1_2.
Definition f3_2 := fuga 3 2 _2_3.
Check f2_1 + f3_2.
(* nat_of_hoge f2_1 + nat_of_hoge f3_2 *)
(* : nat *)
Eval compute in f2_1 + f3_2.
(* = 3 *)
(* : nat *)verilog kernel_is_group.v
kernel_is_group.v
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Arguments belongs {M} x P /.
Definition map {M M' : Type} f (A : set M) (B : set M') :=
forall x, belongs x A -> belongs (f x) B.
Arguments map {M M'} f A B /.
Class group (M : Type) := {
cset : set M;
id : M;
id_belongs : belongs id cset;
bin : M -> M -> M;
inverse : M -> M;
inv_belongs : forall g, belongs g cset -> belongs (inverse g) cset;
entire : forall x y, belongs x cset -> belongs y cset -> belongs (bin x y) cset;
assoc : forall x y z, bin x (bin y z) = bin (bin x y) z;
idR : forall g, bin g id = g;
idL : forall g, bin id g = g;
invR : forall g, bin g (inverse g) = id;
invL : forall g, bin (inverse g) g = id
}.
Lemma both_sides_L : forall {M : Type} (bin : M -> M -> M) (x y z : M),
x = y -> bin z x = bin z y.
Proof.
intros.
rewrite H.
reflexivity.
Qed.
Lemma both_sides_R : forall {M : Type} (bin : M -> M -> M) (x y z : M),
x = y -> bin x z = bin y z.
Proof.
intros.
rewrite H.
reflexivity.
Qed.
Lemma id_inverse_eq_id : forall {M : Type} (G : group M),
@inverse M G (@id M G) = @id M G.
Proof.
intros.
assert (H := @idR M G (@id M G)).
apply (both_sides_L (@bin M G))
with (z := (@inverse M G (@id M G))) in H.
rewrite (@invL M G (@id M G)) in H.
rewrite (@assoc M G (@inverse M G (@id M G)) (@id M G) (@id M G)) in H.
rewrite (@idR M G (@inverse M G (@id M G))) in H.
rewrite (@idR M G (@inverse M G (@id M G))) in H.
assumption.
Qed.
Structure hom M G M' G' := {
hom_f : M -> M';
hom_is_map : map hom_f (@cset M G) (@cset M' G');
hom_law : forall x y, hom_f (@bin M G x y) = @bin M' G' (hom_f x) (hom_f y)
}.
Definition kernel {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G') : set M :=
fun x => hom_f M G M' G' h x = @id M' G'.
Arguments kernel {M M'} G G' h /.
Theorem hom_id_map_id : forall {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G'),
hom_f M G M' G' h (@id M G) = @id M' G'.
Proof.
intros.
assert (hom_f M G M' G' h (@id M G) = hom_f M G M' G' h (@bin M G (@id M G) (@id M G)))
as f_id_G_eq_f__id_G_id_G
by (rewrite (@idR M G (@id M G)); reflexivity).
rewrite (hom_law M G M' G' h (@id M G) (@id M G)) in f_id_G_eq_f__id_G_id_G.
rename f_id_G_eq_f__id_G_id_G into f_id_G_eq_f_id_G_f_id_G.
apply (both_sides_L (@bin M' G') (hom_f M G M' G' h (@id M G)) (@bin M' G' (hom_f M G M' G' h (@id M G)) (hom_f M G M' G' h (@id M G))) (@inverse M' G' (hom_f M G M' G' h (@id M G))))
in f_id_G_eq_f_id_G_f_id_G.
rename f_id_G_eq_f_id_G_f_id_G into inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rewrite (@assoc M' G' (@inverse M' G' (hom_f M G M' G' h (@id M G))) (hom_f M G M' G' h (@id M G)) (hom_f M G M' G' h (@id M G)))
in inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rewrite (@invL M' G' (hom_f M G M' G' h (@id M G)))
in inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rename inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G
into f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rewrite (@idL M' G' (hom_f M G M' G' h (@id M G))) in f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
symmetry.
assumption.
Qed.
Theorem hom_inverse_map_inverse : forall {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G'),
forall x, hom_f M G M' G' h (@inverse M G x) = @inverse M' G' (hom_f M G M' G' h x).
Proof.
intros.
assert (f_id_G_eq_id_G' := hom_id_map_id G G' h).
rewrite <- (@invR M G x) in f_id_G_eq_id_G'.
rename f_id_G_eq_id_G' into f_x_x'_eq_id_G'.
rewrite (hom_law M G M' G' h x (@inverse M G x)) in f_x_x'_eq_id_G'.
rename f_x_x'_eq_id_G' into f_x_f_x'_eq_id_G'.
apply (both_sides_L (@bin M' G'))
with (z:=(@inverse M' G' (hom_f M G M' G' h x)))
in f_x_f_x'_eq_id_G'
as f_x'_f_x_f_x'_eq_f_x'_id_G'.
rewrite (@assoc M' G' (@inverse M' G' (hom_f M G M' G' h x)) (hom_f M G M' G' h x) (hom_f M G M' G' h (@inverse M G x))) in f_x'_f_x_f_x'_eq_f_x'_id_G'.
rewrite (@idR M' G' (@inverse M' G' (hom_f M G M' G' h x)))
in f_x'_f_x_f_x'_eq_f_x'_id_G'.
rename f_x'_f_x_f_x'_eq_f_x'_id_G' into f_x'_f_x_f_x'_eq_f_x'.
rewrite (@invL M' G' (hom_f M G M' G' h x)) in f_x'_f_x_f_x'_eq_f_x'.
rename f_x'_f_x_f_x'_eq_f_x' into id_G'_f_x'_eq_f_x'.
rewrite (@idL M' G' (hom_f M G M' G' h (@inverse M G x))) in id_G'_f_x'_eq_f_x'.
rename id_G'_f_x'_eq_f_x' into f_x'_eq_f_x'.
assumption.
Qed.
Theorem kernel_is_entire : forall {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G'),
forall x y, belongs x (kernel G G' h) -> belongs y (kernel G G' h) -> belongs (@bin M G x y) (kernel G G' h).
Proof.
simpl. intros.
assert (f_xy_eq_fx_fy := hom_law M G M' G' h x y).
rewrite H in f_xy_eq_fx_fy.
rewrite H0 in f_xy_eq_fx_fy.
rename f_xy_eq_fx_fy into f_xy_eq_id_G'_id_G'.
rewrite (@idR M' G' (@id M' G')) in f_xy_eq_id_G'_id_G'.
assumption.
Qed.
Theorem kernel_has_inverse : forall {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G'),
forall x, belongs x (kernel G G' h) -> belongs (@inverse M G x) (kernel G G' h).
Proof.
simpl. intros.
rewrite (hom_inverse_map_inverse G G' h x).
rewrite H.
rewrite id_inverse_eq_id.
reflexivity.
Qed.
Section kernel_G.
Variables M M': Type.
Variables G : group M.
Variables G' : group M'.
Variables h : hom M G M' G'.
Instance kernel_group : group M := { cset := kernel G G' h }.
Proof.
-
apply id.
-
apply hom_id_map_id.
-
apply bin.
-
apply inverse.
-
intros.
apply (kernel_has_inverse G G' h g H).
-
intros.
apply (kernel_is_entire G G' h x y H H0).
-
apply assoc.
-
apply idR.
-
apply idL.
-
apply invR.
-
apply invL.
Qed.
End kernel_G.verilog map_rel_example.v
map_rel_example.v
Definition gen_rel (X Y : Type) := X -> Y -> Prop.
Definition map_rel {X Y : Type} (R : gen_rel X Y) :=
forall x x', x = x' -> forall y y', R x y -> R x' y' -> y = y'.
Arguments map_rel {X Y} R/.
Definition map_rel' {X Y : Type} (R : gen_rel X Y) :=
forall x, exists! y, R x y.
Arguments map_rel' {X Y} R/.
Inductive hoge : nat -> nat -> Prop :=
| hoge_1_2 : hoge 1 2
| hoge_1_3 : hoge 1 3.
Theorem hoge_is_not_map_rel : ~ map_rel hoge.
Proof.
simpl.
intro.
specialize H with (x:=1) (x':=1).
assert (1 = 1) by reflexivity.
assert (H1 := H H0 2 3).
assert (H2 := H1 hoge_1_2 hoge_1_3).
discriminate.
Qed.
Theorem hoge_is_not_map_rel' : ~ map_rel' hoge.
Proof.
simpl.
intro.
specialize H with (x:=1).
inversion H.
inversion H0.
inversion H1.
-
assert (H3 := H2 3 hoge_1_3).
rewrite H3 in H4.
discriminate.
-
assert (H3 := H2 2 hoge_1_2).
rewrite H3 in H4.
discriminate.
Qed.verilog bijection_iff_has_inverse.v
bijection_iff_has_inverse.v
Definition relation (X Y : Type) := X -> Y -> Prop.
Structure map X Y := {
R : relation X Y;
map_law : forall x, exists! y, R x y
}.
Definition is_map {X Y : Type} (R : relation X Y) :=
forall x, exists! y, R x y.
Definition is_injection {X Y : Type} (f : map X Y) :=
forall x x' y, R X Y f x y /\ R X Y f x' y -> x = x'.
(* forall x, exists! y, R X Y f x y. *)
Definition is_surjection {X Y : Type} (f : map X Y) :=
forall y, exists x, R X Y f x y.
Definition is_bijection {X Y : Type} (f : map X Y) :=
is_injection f /\ is_surjection f.
Definition has_inverse {X Y : Type} (f : map X Y) :=
forall y, exists! x, R X Y f x y.
Theorem bijection_iff_has_inverse : forall {X Y : Type} (f : map X Y),
is_bijection f <-> has_inverse f.
Proof.
intros.
split; intros.
- (* -> *)
inversion H as [inj sur_]. clear H.
unfold is_injection in inj.
unfold is_surjection in sur_.
unfold has_inverse.
intros.
specialize sur_ with y.
inversion sur_ as [x sur]. clear sur_.
exists x.
split.
+
assumption.
+
intros.
specialize inj with (x := x) (x' := x') (y := y).
auto.
- (* <- *)
split.
+ (* injection *)
unfold is_injection.
intros.
unfold has_inverse in H.
specialize H with y.
inversion H.
inversion H1.
assert (H4:=H3).
specialize H3 with x.
specialize H4 with x'.
inversion H0.
apply H3 in H5.
apply H4 in H6.
rewrite <- H5.
rewrite <- H6.
reflexivity.
+ (* surjection *)
unfold is_surjection.
unfold has_inverse in H.
intro.
specialize H with y.
inversion H.
exists x.
inversion H0.
assumption.
Qed.verilog group_defined_structure.v
group_defined_structure.v
Structure group M := {
id : M;
bin : M -> M -> M;
inverse : M -> M;
assoc : forall x y z, bin x (bin y z) = bin (bin x y) z;
idR : forall g, bin g id = g;
idL : forall g, bin id g = g;
invR : forall g, bin g (inverse g) = id;
invL : forall g, bin (inverse g) g = id
}.
Structure hom M G M' G' := {
f : M -> M';
hom_law : forall x y, f (bin M G x y) = bin M' G' (f x) (f y)
}.
Lemma both_sides_L : forall {M : Type} (bin : M -> M -> M) (x y z : M),
x = y -> bin z x = bin z y.
Proof.
intros.
rewrite H.
reflexivity.
Qed.
Example hom_id_map_id : forall {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G'),
f M G M' G' h (id M G) = id M' G'.
Proof.
intros.
assert (f M G M' G' h (id M G) = f M G M' G' h (bin M G (id M G) (id M G)))
as f_id_G_eq_f__id_G_id_G
by (rewrite (idR M G (id M G)); reflexivity).
rewrite (hom_law M G M' G' h (id M G) (id M G)) in f_id_G_eq_f__id_G_id_G.
rename f_id_G_eq_f__id_G_id_G into f_id_G_eq_f_id_G_f_id_G.
apply (both_sides_L (bin M' G') (f M G M' G' h (id M G)) (bin M' G' (f M G M' G' h (id M G)) (f M G M' G' h (id M G))) (inverse M' G' (f M G M' G' h (id M G))))
in f_id_G_eq_f_id_G_f_id_G.
rename f_id_G_eq_f_id_G_f_id_G into inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rewrite (assoc M' G' (inverse M' G' (f M G M' G' h (id M G))) (f M G M' G' h (id M G)) (f M G M' G' h (id M G)))
in inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rewrite (invL M' G' (f M G M' G' h (id M G)))
in inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rename inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G
into f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
rewrite (idL M' G' (f M G M' G' h (id M G))) in f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
symmetry.
assumption.
Qed.verilog symmetric_group.v
symmetric_group.v
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Definition subset {M : Type} (S T : set M) :=
forall s, belongs s S -> belongs s T.
Definition id {M : Type} (S : set M) (id : M) (bin : M -> M -> M) :=
forall s, belongs s S -> bin s id = s /\ bin id s = s.
Definition identity {M : Type} (S : set M) (bin : M -> M -> M) :=
exists e, id S e bin.
Definition inverse {M : Type} (S : set M) (s s' : M) (bin : M -> M -> M) :=
belongs s' S ->
id S (bin s s') bin /\ id S (bin s' s) bin.
Definition inversible {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall s, belongs s S -> exists s', inverse S s s' bin.
Definition associative {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall a b c,
belongs a S ->
belongs b S ->
belongs c S ->
bin a (bin b c) = bin (bin a b) c.
Definition entire_property {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall x y, belongs x S -> belongs y S -> belongs (bin x y) S.
Definition magma {M : Type} (S : set M) bin :=
entire_property S bin.
Definition semigroup {M : Type} (S : set M) bin :=
magma S bin /\ associative S bin.
Definition monoid {M : Type} (S : set M) bin :=
semigroup S bin /\ identity S bin.
Definition group {M : Type} (S : set M) bin :=
monoid S bin /\ inversible S bin.
Inductive S :=
| a : S
| b : S.
Definition f0 (s : S) :=
match s with
| a => a
| b => b
end.
Definition f1 (s : S) :=
match s with
| a => b
| b => a
end.
Definition comp (f' f: S -> S) :=
fun s => f' (f s).
Definition S_2 := (fun f => f = f0 \/ f = f1).
Axiom extensionality : forall {X Y:Type} (x:X) (f g:X->Y),
f x = g x -> f = g.
Theorem S_2_is_group : group S_2 comp.
Proof.
unfold group,monoid,semigroup.
split.
-
split.
+
split.
*
unfold magma,entire_property,belongs,S_2.
intros.
inversion H; clear H.
--
inversion H0; clear H0.
++
left.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
++
right.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
--
inversion H0; clear H0.
++
right.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
++
left.
rewrite H. rewrite H1.
apply (extensionality a).
reflexivity.
*
unfold associative,belongs,S_2.
intros.
inversion H; clear H.
--
inversion H0; clear H0.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H0; clear H0.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
inversion H1; clear H1.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
**
rewrite H. rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
+
unfold identity,id,belongs,S_2.
exists f0.
intros.
inversion H; clear H.
*
split.
--
rewrite H0.
apply (extensionality a).
reflexivity.
--
rewrite H0.
apply (extensionality a).
reflexivity.
*
split.
--
rewrite H0.
apply (extensionality a).
reflexivity.
--
rewrite H0.
apply (extensionality a).
reflexivity.
-
unfold inversible,inverse,id,belongs,S_2.
intros.
inversion H; clear H.
+
exists f0.
intros.
split; intros.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
+
exists f1.
intros.
split; intros.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
*
split.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
--
inversion H1; clear H1.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
++
rewrite H0. rewrite H2.
apply (extensionality a).
reflexivity.
Qed.verilog simple_set_example.v
simple_set_example.v
Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Definition subset {M : Type} (S T : set M) :=
forall s, belongs s S -> belongs s T.
Definition id {M : Type} (S : set M) (id : M) (bin : M -> M -> M) :=
forall s, belongs s S -> bin s id = s /\ bin id s = s.
Axiom id_belongs : forall {M : Type} (S : set M) (id_ : M) bin,
id S id_ bin -> belongs id_ S.
Definition identity {M : Type} (S : set M) (bin : M -> M -> M) :=
exists e, id S e bin.
Definition inverse {M : Type} (S : set M) (s s' : M) (bin : M -> M -> M) :=
belongs s S ->
belongs s' S ->
id S (bin s s') bin /\ id S (bin s' s) bin.
Definition inversible {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall s, exists s', inverse S s s' bin.
Definition associative {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall a b c,
belongs a S ->
belongs b S ->
belongs c S ->
bin a (bin b c) = bin (bin a b) c.
Definition entire_property {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
forall x y, belongs x S -> belongs y S -> belongs (bin x y) S.
Definition magma {M : Type} (S : set M) bin :=
entire_property S bin.
Definition semigroup {M : Type} (S : set M) bin :=
magma S bin /\ associative S bin.
Definition monoid {M : Type} (S : set M) bin :=
semigroup S bin /\ identity S bin.
Axiom monoid_has_id : forall {M:Type} (S : set M) bin,
monoid S bin -> exists id_S, belongs id_S S /\ id S id_S bin.
Definition group {M : Type} (S : set M) bin :=
monoid S bin /\ inversible S bin.
Axiom group_inverse_belongs : forall {M:Type} (S : set M) bin,
forall g g', group S bin -> inverse S g g' bin -> belongs g S /\ belongs g' S.
Definition subgroup {M : Type} (H G : set M) bin :=
subset H G /\ group H bin /\ group G bin.
Theorem subgroup_eq_condition {M : Type} : forall (H G : set M) bin,
subset H G ->
group G bin -> (
group H bin <-> (
(forall id_G, id G id_G bin -> belongs id_G H) /\
entire_property H bin /\
(forall x, exists x', belongs x H -> inverse H x x' bin)
)
).
Proof.
intros H G bin H_subsetHG GisGroup.
split.
- (* -> *)
intros HisGroup.
split.
+
intros id_G H_id_G.
assert (HisGroup_ := HisGroup).
unfold group in HisGroup_.
inversion HisGroup_ as [HisMonoid _]. clear HisGroup_.
apply monoid_has_id in HisMonoid.
inversion HisMonoid as [id_H H_identity]. clear HisMonoid.
(* created id_H *)
unfold id in H_identity.
inversion H_identity as [H_idH_in_H H_identity_]. clear H_identity.
assert (H_idH_in_H_:=H_idH_in_H).
assert (H_identity__:=H_identity_).
specialize H_identity_ with id_H.
apply H_identity_ in H_idH_in_H. clear H_identity_.
inversion H_idH_in_H as [H_idHidH_eq_idH _]. clear H_idH_in_H.
(* created bin id_H id_H = id_H *)
assert (GisGroup_ := GisGroup).
unfold group,monoid,semigroup,identity,id,inversible in GisGroup_.
inversion GisGroup_ as [[[_ G_assoc] _] G_inverse]. clear GisGroup_.
specialize G_inverse with id_H.
inversion G_inverse as [id_H' G_inverse__]. clear G_inverse.
(* created id_H' *)
assert (H_idH'idHidH_eq_idH'idH : bin id_H' (bin id_H id_H) = bin id_H' (id_H))
by (rewrite H_idHidH_eq_idH; reflexivity).
(* created bin id_H' (bin id_H id_H) = bin id_H' id_H *)
assert (G_inverse_:=G_inverse__).
apply (group_inverse_belongs G bin id_H id_H' GisGroup) in G_inverse__.
inversion G_inverse__ as [id_H_in_G id_H'_in_G].
unfold inverse,id in G_inverse_.
apply (G_inverse_ id_H_in_G) in id_H'_in_G. clear G_inverse_.
inversion id_H'_in_G as [_ G_inv0]. clear id_H'_in_G.
specialize G_inv0 with id_G.
assert (H_id_G__ := H_id_G).
apply id_belongs in H_id_G__.
apply G_inv0 in H_id_G__.
inversion H_id_G__ as [G_inv2_1 G_inv2_2]. clear H_id_G__.
assert (H_id_G_ := H_id_G).
unfold id in H_id_G.
specialize H_id_G with (bin id_H' id_H).
specialize H_identity__ with id_H'.
unfold group,monoid,semigroup,magma,entire_property in GisGroup.
inversion GisGroup as [[[G_entire_prop _] _] _]. clear GisGroup.
inversion G_inverse__ as [G_inv2 G_inv3].
assert (G_inv2_:=G_inv2).
apply (G_entire_prop id_H' id_H G_inv3) in G_inv2.
apply H_id_G in G_inv2.
inversion G_inv2 as [_ H_id_G0]. clear G_inv2.
rewrite H_id_G0 in G_inv2_1.
rewrite G_inv2_1 in H_idH'idHidH_eq_idH'idH.
(* created bin id_H' (bin id_H id_H) = id_G *)
assert (G_inv0_:=G_inv0).
unfold associative in G_assoc.
specialize G_assoc with (a:=id_H') (b:=id_H) (c:=id_H).
assert (G_inv0__:=G_inv0_).
rewrite (G_assoc G_inv3 G_inv2_ G_inv2_) in H_idH'idHidH_eq_idH'idH.
(* created bin (bin id_H' id_H) id_H) = id_G *)
rewrite G_inv2_1 in H_idH'idHidH_eq_idH'idH.
(* created bin (bin id_H' id_H) id_H) = id_G *)
unfold id in H_id_G_.
specialize H_id_G_ with id_H.
apply H_id_G_ in id_H_in_G.
inversion id_H_in_G as [_ idGidH_eq_idH].
rewrite idGidH_eq_idH in H_idH'idHidH_eq_idH'idH.
(* created id_H = id_G *)
rewrite <- H_idH'idHidH_eq_idH'idH.
assumption.
+
split.
*
unfold group,monoid,semigroup,magma in HisGroup.
inversion HisGroup as [[[H_entire _] _] _].
assumption.
*
intros x_H H_x_H.
unfold group in HisGroup.
inversion HisGroup as [_ H_inverse].
unfold inversible,inverse in H_inverse.
unfold inverse.
intros x.
specialize H_inverse with x.
inversion H_inverse.
exists x0.
intros H1.
assumption.
- (* <- *)
intros H_123.
unfold group,monoid,semigroup.
split.
+
split.
*
split.
--
inversion H_123 as [_ [H_entire _]].
assumption.
--
unfold group,monoid,semigroup in GisGroup.
inversion GisGroup as [[[_ G_assoc] _] _]. clear GisGroup.
unfold associative in *.
intros a b c ainH binH cinH.
specialize G_assoc with a b c.
apply H_subsetHG in ainH.
apply H_subsetHG in binH.
apply H_subsetHG in cinH.
apply (G_assoc ainH binH) in cinH.
assumption.
*
unfold group,monoid,identity in GisGroup.
inversion GisGroup as [[_ G_identity] _].
inversion G_identity as [id_G G_identity_].
unfold identity.
exists id_G.
unfold id in G_identity_.
unfold id.
intros s H_s_in_H.
specialize G_identity_ with s.
apply H_subsetHG in H_s_in_H.
apply G_identity_ in H_s_in_H.
assumption.
+
unfold inversible, inverse.
intros s.
inversion H_123 as [_ [_ H_3]].
specialize H_3 with s.
inversion H_3 as [s'].
exists s'.
unfold inverse in H0.
intros.
apply (H0 H1 H1 H2).
Qed.
verilog inverse_map_uniq.v
inverse_map_uniq.v
Definition obj := Type.
Inductive map : Type :=
| Id : obj -> map
| Diff : obj -> obj -> map
| Comp : map -> map -> map.
Inductive hom : map -> obj -> obj -> Prop :=
| HomId : forall f a,
f = Id a -> hom f a a
| HomDiff : forall f a b,
f = Diff a b -> hom f a b
| HomComp : forall f g h a b c,
f = Comp g h ->
hom g a b ->
hom h b c ->
hom f a c.
Inductive map_eq : map -> map -> Prop :=
| Com : forall f g,
map_eq f g -> map_eq g f
| Eq : forall f, map_eq f f
| CompAssoc : forall f g h,
map_eq
(Comp (Comp h g) f)
(Comp h (Comp g f))
| IdL : forall a b f g,
hom f a b ->
map_eq (Comp (Id b) f) g ->
map_eq f g
| IdR : forall a b f g,
hom f a b ->
map_eq (Comp f (Id a)) g ->
map_eq f g.
Definition inverse a b f g :=
hom f a b /\
hom g b a /\
Comp f g = Id b /\
Comp g f = Id a.
Lemma inverse_uniq : forall a b (f g g' : map),
inverse a b f g ->
inverse a b f g' ->
map_eq g g'.
Proof.
intros.
inversion H. clear H.
inversion H0. clear H0.
inversion H2. clear H2.
inversion H3. clear H3.
inversion H4. clear H4.
inversion H5. clear H5.
assert (map_eq (Comp (Comp g f) g')
(Comp g (Comp f g'))) by constructor.
rewrite H6 in H5.
rewrite H4 in H5.
apply (IdL b a g' (Comp g (Id b)) H2) in H5.
apply Com in H5.
apply (IdR b a g g' H0) in H5.
assumption.
Qed.verilog mem模型
mem_model.sv
class crypto_core_memory_top::uvm_object
memory_manager_cfg_base ns_mem_man_cfg, s_mem_man_cfg, qad_mem_man_cfg;
memory_manager_base_abstract ddt_ns_mem_man, ddt_s_mem_man, ddt_qad_mem_man;
memory_manager_base_abstract dst_ns_mem_man, dst_s_mem_man, dst_qad_mem_man;
... dst_ns_mem_man
function get_mem_man (string mem_type, ns)
case mem_type:
"ddt" :
case ns:
MEM_SEC : return ddt_s_mem_man
MEM_NONSEC: return ddt_ns_mem_man
MEM_QAD: return ddt_qad_mem_man
endcase
...
task malloc_ddt_mem (ref memory_acc_block block, size, align, s_addr, ns, trans_args)
memory_manager_base_abstract mem_man = get_mem_man ("ddt", ns);
mem_man.malloc (acc_block, size, align, s_addr, args);
task malloc_src (ref memory_acc_block acc_block, size, align, s_addr, ns, trans_arg)
memory_manager_base_abstract mem_man = get_mem_man ("src", ns);
mem_man.malloc (acc_block, size, align, s_addr, args);
class crypot_memory_top extends crypto_core_mem_top
static crypot_qsb_mem_manager ns_mem_man, s_mem_man, qad_mem_man
function init (core_id, memory_manager_base_abstract ns_mem, s_mem, qad_mem,
memory_manager_cfg_base ns_mem_cfg, s_mem_cfg, qad_mem_cfg)
this.ns_mem_man_cfg = ns_mem_man_cfg
...
ns_man_man == null?
ns_mem_man = crypot_qsb_mem_manager::create (...)
ns_mem_man.configurate (ns_mem, ns_mem_man_cfg)
ns_mem_man.sec = NON_SECURE
ddt_ns_mem_man = ns_mem_man
dst_ns_mem_man = ns_mem_man
src_ns_mem_man = ns_mem_man
s_mem_man == null ?
...
qad_mem_man == null ?
...
class crypto_qsb_memory_manager extends memory_manager_base
sec_type sec
function va2pa (va, memory_translation_args_base_abstract args)
crypto_core_mem_translation_args _args
$cast (_args || args==null)?
_args = create(...)
pa = smmu_subenv.va2pa(va, _args.stram_id, 0, sec)
function pa2va (pa, args)
return pa
class crypto_qsb_memory_model extends memory_model_base_abstract
function write (addr, MEM_BYTE data)
for (i=0..3)
nvs_qsb_axi_memory::mem_space_0[addr[63:2], 2'b0][8*i +:8] = data
function MEM_BYTE data read (addr)
return nvs_qsb_axi_memory::mem_space_0[addr[63:2], 2'b0][8*addr[1:0] +:8] = data
\!h user_code
class user_test
class user_seq
crypto_core_memory_top mem_man
task pre_start
get_config_db mem_man
task some_task
mem_acc_block _mem
ddt_obj ddt
...
//call crypto_core_memory_top.malloc_src. malloc a new mem_block
mem_man.malloc_src (_mem, len, addr, sec, ddt.mem.trans_args)
ddt.set_mem(_mem)
ddt.do_something()
class ddt_obj
memory_access_block mem
function set_mem (memory_access_block mem)
this.mem = mem
function do_something()
mem.write(...)
verilog ADS 805驱动代码
ADS 805驱动代码
ads805_intf.v
/**
* @brief ads805 interface
* @param [out] ad_dclk AD时钟
* @note 6个时钟后才是本次触发的对应值
*/
module ads805_intf #(
parameter DATA_WIDTH = 12
) (
input clk,
input rst_n,
input en_pulse,
input start,
input [DATA_WIDTH-1:0] ad_dout,
output reg ad_dclk,
output reg [DATA_WIDTH-1:0] ad_res,
output reg drdy
);
localparam HIG = 1'b1;
localparam LOW = 1'b0;
localparam NOT_READY = 1'b0;
localparam READY = 1'b1;
localparam STATE_WIDTH = 3;
localparam S_SCAN_WAIT_AD_UP = 3'b001;
localparam S_SCAN_WAIT_AD_UPDOWN_DCLK = 3'b010;
localparam S_SCAN_WAIT_AD_UPUP_DCLK = 3'b100;
reg[STATE_WIDTH-1:0] state;
reg[STATE_WIDTH-1:0] next_state;
initial
begin
ad_dclk <= 0;
ad_res <= 0;
state <= 0;
drdy <= 0;
end
always @ (negedge rst_n or posedge clk)
begin
if (!rst_n)
state <= S_SCAN_WAIT_AD_UP;
else if (en_pulse)
state <= next_state;
end
always @ (*)
begin
next_state = S_SCAN_WAIT_AD_UP;
case (state)
S_SCAN_WAIT_AD_UP:
begin
if(start)
next_state = S_SCAN_WAIT_AD_UPUP_DCLK;
else
next_state = S_SCAN_WAIT_AD_UP;
end
S_SCAN_WAIT_AD_UPUP_DCLK:
begin
next_state = S_SCAN_WAIT_AD_UPDOWN_DCLK;
end
S_SCAN_WAIT_AD_UPDOWN_DCLK:
begin
if(start)
next_state = S_SCAN_WAIT_AD_UPUP_DCLK;
else
next_state = S_SCAN_WAIT_AD_UP;
end
default:
begin
next_state = S_SCAN_WAIT_AD_UP;
end
endcase
end
always @ (negedge rst_n or posedge clk)
begin
if (!rst_n)
begin
ad_dclk <= LOW;
ad_res <= {DATA_WIDTH{1'b0}};
drdy <= NOT_READY;
end
else if (en_pulse)
begin
case(next_state)
S_SCAN_WAIT_AD_UP:
begin
ad_dclk <= LOW;
drdy <= NOT_READY;
end
S_SCAN_WAIT_AD_UPUP_DCLK:
begin
ad_dclk <= HIG;
drdy <= NOT_READY;
end
S_SCAN_WAIT_AD_UPDOWN_DCLK:
begin
ad_dclk <= LOW;
ad_res <= ad_dout;
drdy <= READY;
end
default:
begin
ad_dclk <= LOW;
ad_res <= {DATA_WIDTH{1'b0}};
drdy <= NOT_READY;
end
endcase
end
end
endmodule