Classic.lp

// PRELUDE ##############
// Définitions intuitioniste nécessaires pour illustrer le problème dans Classic.

constant symbol Prop : TYPE;

injective symbol π : Prop → TYPE; // `p

constant symbol ∨ : Prop → Prop → Prop; notation ∨ infix left 6; // \/ or \vee

constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);
constant symbol ∨ᵢ₂ [p q] : π q → π (p ∨ q);
symbol ∨ₑ [p q r] : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;

constant symbol ⊥ : Prop; // \bot
constant symbol ⇒ : Prop → Prop → Prop; notation ⇒ infix right 5; // =>

rule π ($p ⇒ $q) ↪ π $p → π $q;
symbol ¬ p ≔ p ⇒ ⊥; notation ¬ prefix 35;

// CLASSIC ############

// Une preuve classique est une preuve intuitioniste avec une double négation de la proposition.
// Mon problène avec cette définition est quelle introduit des doubles négations partout dans les preuves
// des lemmes classiques.
injective symbol πᶜ p ≔ π (¬ ¬ p);

// Quelque opérateurs classics
symbol ∨ᶜ p q ≔ ¬ ¬ p ∨ ¬ ¬ q; notation ∨ᶜ infix right 20;
symbol ⇒ᶜ p q ≔ ¬ ¬ p ⇒ ¬ ¬ q; notation ⇒ᶜ infix right 10;

// Ici on cherche bien à prouver cette règle de la déduction naturel classique
// avec la définition de πᶜ p = π (¬ ¬ p).
opaque symbol ∨ᶜᵢ₁ [p q] : πᶜ p → πᶜ (p ∨ᶜ q) ≔
begin
    assume p q Hnnp;
    assume Hnnp_or_nnq;
    apply Hnnp_or_nnq;
    apply ∨ᵢ₁;
    refine Hnnp;
end;

// Ici je voudrais faire une preuve du Lemme imply_to_or sans que la définition de πᶜ p = π (¬ ¬ p)
// soit unfold et juste en utilisant les règles de la déduction naturel classique
opaque symbol imply_to_or [p q] : πᶜ (p ⇒ᶜ q) → πᶜ ((¬ p) ∨ᶜ q) ≔
begin
    assume p q Hp;
    apply ∨ᶜᵢ₁; 
    // Pour illustrer le problème (même si on ne voudrait pas faire ca pour prouver ce Lemme)
    // si on applique le Lemme ∨ᵢ₁ on a l'erreur: [⊥] and [¬ (¬ p ∨ᶜ q) ⇒ ⊥] are not unifiable.
    // Lambdapi va automatiquement unfold la définition de πᶜ.
    // J'aurais aimé qu'il n'unfold pas la définition et que l'application de ∨ᶜᵢ₁ sur πᶜ (¬ p ∨ᶜ q)
    // me donne πᶜ (¬ p)
    
end;

// Une idée que j'avais aurait été de créer un autre symbole πᶜ opaque/sans défintion
// puis avoir une règle de réécriture mais ca ne marche pas car Lambdapi va tout réécrire automatiquement en πᶜ p;
injective symbol πᶜₒ: Prop → TYPE;
rule πᶜₒ $p ↪ πᶜ $p;

// 2eme idée était de faire un symbol opaque avec une définition, mais alors il devient impossible
// de prouver la règle de déduction naturel ∨ᶜᵢ₁ car j'ai besoin de la double négation pour elle.
opaque injective symbol πᶜ' p ≔ π (¬ ¬ p); 

// Ma question est comment puis-je définir un symbole avec une définition,
// puis plus tard la rendre opaque ?
// Pour classic, ce serait de prouver toutes les règles de la déduction naturel classic avec le ¬ ¬
// puis de prouver les autres Lemme comme Pierce, etc en utilisant les les règles de la déduction naturel classique
// mais en oubliant la définition de πᶜ p := π ¬ ¬ p ??