ImpAlg.Dummies

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.ParAlgebras.
Require Import ImpAlg.TensorAlgebras.
Require Import ImpAlg.Combinators.

Section Dummy.
Context `{CL:CompleteLattice}.

Definition partop (a b:X):= ⊤.
Definition tensorbot (a b:X):= ⊥.
Definition negbot (a:X):=⊥.
Definition negtop (a:X):=⊤.
Definition arrowtop (a b:X):=⊤.
Definition arrow_r (a b:X):=b.

Dummy Structures



Global Instance dummy_imp_r : ImplicativeStructure := { arrow:= arrow_r}.
Proof.
- unfold arrow_r;intros; intuition.
- unfold arrow_r;intros; intuition.
- unfold arrow_r;intros; intuition.
  apply meet_same_set. unfold arrow_set_r. auto_same_setX X.
Defined.

Global Instance dummy_imp_top : ImplicativeStructure := { arrow:= arrowtop}.
Proof.
- unfold arrowtop;intros; intuition.
- unfold arrowtop;intros; intuition.
- unfold arrowtop;intros; intuition.
  apply ord_antisym;[|apply top_max].
  apply meet_intro. intros x (_,(_,H));subst x;reflexivity.
Defined.

Counter example to ⊢t:A → t = A

In this dummy implicative structure, any application is equal to ⊥, while any abstraction is equal to ⊤

Lemma dummy_top_app: ∀ a b, (@ImplicativeStructures.app _ _ _ _ dummy_imp_top a b = ⊥).
Proof.
  intros a b.
  apply meet_same_set.
  auto_same_setX X;intuition.
  apply top_max.
Qed.

Lemma dummy_top_abs: ∀ f, (@ImplicativeStructures.abs _ _ _ _ dummy_imp_top f = ⊤).
Proof.
  intros f.
  apply ord_antisym;auto.
  apply meet_intro;intros x [a H];subst.
  reflexivity.
Qed.

In particular, we can show that II ≠ ⋂a (a→a) = I

Definition Idum:=(@Id _ _ _ _ dummy_imp_top).
Lemma II_neq_I: ⊥ ≠ ⊤ → Idum @Idum ≠ Idum.
Proof.
  intro H.
  rewrite dummy_top_app.
  unfold Idum.
  rewrite lambda_Id,dummy_top_abs.
  assumption.
Qed.

Definition Kdum:=(@K _ _ _ _ dummy_imp_top).
Definition Sdum:=(@S _ _ _ _ dummy_imp_top).
Lemma I_neq_SKK_dum : ⊥ ≠ ⊤ → ¬ (Idum ≤ (Sdum @ Kdum) @ Kdum).
Proof.
intros H.
unfold Idum. rewrite lambda_Id,dummy_top_abs,dummy_top_app.
contradict H. apply ord_antisym;auto.
Qed.

Dummy ⅋-algebra

Global Instance dummy_par: ParStructure := { par := partop; pneg:=negbot}.
Proof.
intros; intuition.
- unfold partop;intros; intuition.
- unfold negbot;intros; intuition.
- unfold partop,par_set_l;intros; intuition.
  apply ord_antisym;[|apply top_max].
  apply meet_intro. intros x (_,(_,H));subst x;reflexivity.
- unfold partop,par_set_r;intros; intuition.
  apply ord_antisym;[|apply top_max].
  apply meet_intro. intros x (_,(_,H));subst x;reflexivity.
- unfold negbot,partop,image_set;intros; intuition.
  apply ord_antisym;[apply bot_min|].
  apply join_intro. intros x (_,(_,H));subst x;reflexivity.
Defined.

Dummy ⨂-algebra

Global Instance dummy_tensor: TensorStructure := { tensor := tensorbot; tneg:=negtop}.
Proof.
intros; intuition.
- unfold tensorbot;intros; intuition.
- unfold negtop;intros; intuition.
- unfold tensorbot,par_set_l;intros; intuition.
  apply ord_antisym;[apply bot_min|].
  apply join_intro. intros x (_,(_,H));subst x;reflexivity.
- unfold tensorbot,par_set_r;intros; intuition.
  apply ord_antisym;[apply bot_min|].
  apply join_intro. intros x (_,(_,H));subst x;reflexivity.
- unfold negtop,tensorbot,image_set;intros; intuition.
  apply ord_antisym;[|apply top_max].
  apply meet_intro. intros x (_,(_,H));subst x;reflexivity.
Defined.

End Dummy.