# Library proofs

Reserved Notation "e =* f" (at level 80).

Kleene algebra axioms with no constants.
Inductive ka_eq : relation expr :=
| ka_tt e f g : (e · (f · g)) =* ((e · f) · g)

| ka_pp e f g : (e + (f + g)) =* ((e + f) + g)
| ka_pc e f : (e + f) =* (f + e)
| ka_pi e : (e + e) =* e

| ka_pt e f g : (e · (f + g)) =* ((e · f) + (e · g))
| ka_tp e f g : ((e + f) · g) =* ((e · g) + (f · g))

where "e =* f" := (ka_eq e f).
Kleene algebra entailments.
Inductive ka_impl : expr relation expr :=
| ka_s3 e f g : ka_impl (f + e·g) (e^*·f) g
| ka_s4 e f g : ka_impl (f + g·e) (f·e^* ) g.

Kleene algebra axioms for untyped constants.
Inductive ka_eq_u : relation expr :=
| kau_t1 e : ka_eq_u (e · 1) e
| kau_1t e : ka_eq_u (1 · e) e
| kau_s1 e : ka_eq_u (1 + e · (e^*) + e ^*) (e^*)
| kau_s2 e : ka_eq_u (1 + (e^*) · e + e^*) (e^*).
Kleene algebra axioms for typed constants.
Inductive ka_eq_t : relation expr :=
| kat_t1 e A : A e ka_eq_t (e · id A) e
| kat_1t e A : A e ka_eq_t (id A · e) e
| kat_s1 e A : A e ka_eq_t (id A + e · (e^*) + e ^*) (e^*)
| kat_s2 e A : A e ka_eq_t (id A + (e^*) · e + e^*) (e^*).

Reserved Notation " ax ⊢ e ≡ f" (at level 80).
Reserved Notation " ax ⊢ e ≤ f" (at level 80).

Inductive eq (ax : relation expr) : relation expr :=
Structural rules
| eq_sym e f : (ax e f) ax f e
| eq_trans e f g : ax e f ax f g ax e g

Congruence
| eq_zero : ax 0 0
| eq_un : ax 1 1
| eq_bot A B : A B ax ( A) ( B)
| eq_id A B : A B ax (id A) (id B)
| eq_var x y : x y ax (var x) (var y)
| eq_vat a : ax (vat a) (vat a)
| eq_plus e f g h : ax e f ax g h ax (e+g) (f+h)
| eq_times e f g h : ax e f ax g h ax (e·g) (f·h)
| eq_star e f : ax e f ax (e^* ) (f^* )
| eq_ν a e f: ax e f ax (ν a e) (ν a f)
| eq_θ p q e f: pq ax e f ax ( p e) ( q f)
| eq_ω a e f: ax e f ax (ω a e) (ω a f)

Kleene algebra without constants
| eq_ka e f : e =* f ax e f
| eq_ka_impl e f g : ax e g ka_impl e f g ax f g

| eq_ax e f : ax e f ax e f
where " ax ⊢ e ≡ f " := (eq ax e f)
and " ax ⊢ e ≤ f " := (eq ax (e+f) f).
For any axiomatic system the eq relation is reflexive.
Lemma eq_refl ax e : ax e e.
For any axiomatic system the eq relation an equivalence relation.
Instance eq_Equiv ax : Equivalence (eq ax).
Lemma eq_expr_eq ax e f : (e == f) ax e f.

Global Instance stronger_ax_proof :
Proper ((@stronger expr) ==> inclusion expr) eq.
Lemma stronger_ax_eq a b : a b a eq b.
Lemma stronger_eq_or_rel_l :
A B, inclusion expr (eq A) (eq (AB)).
Lemma stronger_eq_or_rel_r :
A B, inclusion expr (eq B) (eq (AB)).

Goal ( A B C e f, ABC e f A∨(BC) e f).

For any axiomatic system all operators are morphisms with respect to eq.
Global Instance ν_eq ax a :
Proper (eq ax ==> eq ax) (ν a).
Global Instance ω_eq ax a :
Proper (eq ax ==> eq ax) (ω a).
Global Instance plus_eq ax :
Proper (eq ax ==> eq ax ==> eq ax) plus.
Global Instance times_eq ax :
Proper (eq ax ==> eq ax ==> eq ax) times.
Global Instance θ_eq ax :
Proper (equiv_perm ==> eq ax ==> eq ax) θ.
Global Instance star_eq ax:
Proper (eq ax ==> eq ax) star.
Global Instance bot_equiv_lst_eq ax:
Proper (equiv_lst ==> eq ax) bot.
Global Instance id_equiv_lst_eq ax:
Proper (equiv_lst ==> eq ax) id.

Notation inf ax := (fun x yax x y).
The relation ≤ is antisymmetric with respect to ≡.
Instance inf_antisym ax : Antisymmetric expr (eq ax) (inf ax).

Kleene algebra axioms for 0.
Kleene algebra axioms for ⊥.
Inductive zero_ka_t : relation expr :=
| zero_t_p0 e A : A e zero_ka_t (e + A) e
| zero_t_t0 e A : A e zero_ka_t (e · A) ( A)
| zero_t_0t e A : A e zero_ka_t ( A · e) ( A).

Inductive zero_perm_u : relation expr :=
| eq_θ_0 p : zero_perm_u ( p 0) 0.

Inductive zero_perm_t : relation expr :=
| eq_θ_bot A B p : (B p A) zero_perm_t ( p ›( A)) ( B).
Inductive zero_nom_u : relation expr :=
| equ_ν0 a : zero_nom_u (ν a 0) 0.
derivable from eq_nom_untyped, because a#0
Permutations.
Distributivity laws of ν,ω.
Inductive eq_ν_smpl : relation expr :=
| eq_νp a e f : eq_ν_smpl (ν a (e+f)) (ν a e + ν a f)
| eq_νab a b e : eq_ν_smpl (ν a (ν b e)) (ν b (ν a e)).
Inductive eq_ω_smpl : relation expr :=
| eq_ω_id a A : ~(In a A) eq_ω_smpl (ω a (id A)) (id (a::A))
| eq_ω_p e f a : eq_ω_smpl (ω a (e + f)) (ω a e + ω a f)
| eq_ω_t e f a : eq_ω_smpl (ω a (e · f)) (ω a e · ω a f)
| eq_ω_s e a : eq_ω_smpl (ω a (e^*)) ((ω a e)^*)
| eq_ωω e a b : eq_ω_smpl (ω a (ω b e)) (ω b (ω a e)).

Untyped nominal axioms.
Inductive eq_nom_untyped_p : relation expr :=
| equ_θν' a b e :
a # e eq_nom_untyped_p (ν b e) (ν a ( [a,b]e )).
Inductive eq_nom_untyped_np : relation expr :=
| equ_θν a b e :
a # e eq_nom_untyped_np (ν b e) (ν a ( [a,b]e )).

Inductive eq_nom_untyped : relation expr :=
| equ_νω1 a e :
a # e eq_nom_untyped (ν a e) e
| equ_ν3 a e f :
a # e eq_nom_untyped ((ν a f) · e) (ν a (f · e))
| equ_ν4 a e f :
a # e eq_nom_untyped (e · (ν a f)) (ν a (e · f)).

Typed nominal axioms.
Inductive eq_nom_typed_p : relation expr :=
| eqt_θν' A a b e : A ν a e ¬ In b A
eq_nom_typed_p (ν a e) (ν b ([b,a]e)).
Inductive eq_nom_typed_np : relation expr :=
| eqt_θν A a b e : A ν a e ¬ In b A
eq_nom_typed_np (ν a e) (ν b ([b,a]e)).
Inductive eq_nom_typed : relation expr :=

| eqt_νω1 A a e :
A ν a (ω a e)
eq_nom_typed (ν a (ω a e)) e
| eqt_νω2 e a b :
a b eq_nom_typed (ν a (ω b e)) (ω b (ν a e))
| eqt_ν3 a e f :
eq_nom_typed ((ν a f) · e) (ν a (f · ω a e))
| eqt_ν4 a e f :
eq_nom_typed (e · (ν a f)) (ν a ((ω a e) · f)).

Lemma eqt_ν1 A a :
In a A
eq_nom_typed eq_ω_smpl (ν a (id A)) (id (rm a A)).

Lemma stronger_Ty_zero_ka_t : zero_ka_t ty' zero_ka_t.
Lemma stronger_Ty_ka_eq_t : ka_eq_t ty' ka_eq_t.

Lemma one_star_is_one_u : ka_eq_u 1^* 1.
Lemma one_star_is_one_t A: ka_eq_t (id A)^* (id A).

Lemma zero_nom_u_derivable : zero_nom_u eq_nom_untyped.

Lemma derivable_axioms (ax1 ax2 : relation expr) :
( e f, ax1 e f ax2 e f)
( e f, (ax1ax2) e f ax2 e f).

Type preservation.