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: p ≌q → 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

Additionnal axioms

| 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 (A ∨B)).
Lemma stronger_eq_or_rel_r :
  ∀ A B, inclusion expr (eq B) (eq (A ∨B)).

Goal (∀ A B C e f, A ∨B ∨C ⊢ e ≡ f → A ∨(B ∨C ) ⊢ 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 y ⇒ ax ⊢ x ≤ y).

The relation ≤ is antisymmetric with respect to ≡.

Instance inf_antisym ax : Antisymmetric expr (eq ax) (inf ax).

Kleene algebra axioms for 0.

Inductive zero_ka_u : relation expr :=
| zero_u_p0 e : zero_ka_u (e + 0) e
| zero_u_t0 e : untyped e → zero_ka_u (e · 0) 0
| zero_u_0t e : untyped e → zero_ka_u (0 · e) 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

Inductive zero_nom_t : relation expr :=
| eq_ω _bot a A : ~(In a A ) → zero_nom_t (ω a (⊥ A)) (⊥ (a ::A ))
| eqt_ν0 A a : In a A → zero_nom_t (ν a (⊥ A)) (⊥ (rm a A )).

Notation zero_eq_t := (zero_ka_t ∨ zero_perm_t ∨ zero_nom_t).
Notation zero_eq_u := (zero_ka_u ∨ zero_perm_u ∨ zero_nom_u).

Permutations.

Inductive eq_perm : relation expr :=
| eq_θ_p p e f : eq_perm (‹ p › (e +f )) (‹ p ›e + ‹ p ›f)
| eq_θ_t p e f : eq_perm (‹ p › (e ·f )) (‹ p ›e · ‹ p ›f)
| eq_θ_s p e : eq_perm (‹ p › (e ^* )) ((‹ p ›e )^* )
| eq_θ_ν p a e : eq_perm (‹ p › (ν a e )) (ν (p ⋈a) (‹ p › e))
| eq_θ_θ p' p e : eq_perm (‹ p › (‹ p' › e )) (‹p ++p'› e).

Inductive eq_perm_ω : relation expr :=
| eq_θ_ω p a e : eq_perm_ω (‹ p › (ω a e )) (ω (p ⋈a) (‹ p › e)).

Inductive eq_perm_elim : relation expr:=
| eq_θ_1 p : eq_perm_elim (‹ p ›1) 1
| eq_θ_at p a : eq_perm_elim (‹ p ›(vat a )) (vat (p ⋈ a))
| eq_θ_var p a : eq_perm_elim (‹ p ›(var a )) (var (apply_perm_var p a))
| eq_θ_id A B p : (B ≈ p ⧓ A ) → eq_perm_elim (‹ p ›(id A )) (id B)

| eq_nil_e e : eq_perm_elim (‹[]› e) e.

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, (ax1 ∨ax2 ) ⊢ e ≡ f → ax2 ⊢ e ≡ f ).

Type preservation.