ImpAlg.Dummies

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Sets.Ensembles.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.Combinators.

Section Dummy.
Context `{CL:CompleteLattice}.

Dummy Structures

We define a tactic to ease the proofs that two sets are extentionally equal

Ltac auto_same_set_stepX X:=
  match goal with
  |[ |- _ ≅ _ ] => let x:=fresh "x" in let a := fresh "a" in let H:=fresh "H" in
              unfold image_set,arrow_set_r; split;intro x; try (intros [a H]);intros;unfold In
  |[ H: (∃ _: X, _ = _ ) ∧ ?x = _ |- ∃ _:X, ?x = _] =>
   let b:=fresh "a" in let Ha:=fresh "H" in let Hb:=fresh "H" in
           destruct H as ((b,Hb),Ha);try(later; rewrite Ha,Hb)
  |[ H: ∃ _: X, (_ ∧ ?x = _) |- _] =>
    let b:=fresh "a" in let Ha:=fresh "H" in let Hb:=fresh "H" in
           destruct H as (b,(Hb,Ha));try(subst b);auto
  |[ H: ∃ _: X,_ |- _] => let b:=fresh "a" in let Ha:=fresh "H" in
           destruct H as (b,Ha);try(subst);auto
  |[ H: _ ∧ _ |- _] => let Ha:=fresh "H" in let Hb:=fresh "H" in
           destruct H as (Ha,Hb);try(subst);auto
  |[ H: ?x = _ |- ∃ _ : X, ((∃ _ : X, _ = _) ∧ ?x = _ )] =>
           try(later;split;[later;reflexivity|]);try(rewrite H;now reflexivity)
  |[ H: ?x = _ |- ∃ _ : X,( _ ∧ ?x = _ )] => later;split;[|reflexivity];try(now auto)
  |[ H: ?x = _ |- ∃ _ : X, ?x = _] => later
  |[ H: ?A ?x |- ∃ a : X,( ?A a ∧ ?x = a )] => try(later;split;[|reflexivity]);try(now auto)
  |[ |- ⊓ _ = ⊓ _] => apply meet_same_set
  |[ |- _ = _] => now reflexivity
  end.

Ltac auto_same_setX X:=repeat (auto_same_set_stepX X).

a ↦ b := b

Proposition 6.1

Definition arrow_r (a b:X):=b.

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. auto_same_setX X.
Defined.

a ↦ b := b

Proposition 6.2

Definition arrowtop (a b:X):=⊤.

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

Remark 19 in the paper

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.

End Dummy.