Propositionnel Logic et Proofs

Question

J'essaie de prouver le cas ci-dessous pour une tâche de devoirs et j'ai travaillé des heures là-dessus, toujours pas de chance.

Toutes les suggestions ou commentaires quant à ce que je fais mal?

Answer 1

C'est comment vous prouvez en Coq:

Coq < Theorem curry : forall p q r, ((q /\ p) -> r) -> p -> q -> r. 
1 subgoal 

    ============================ 
    forall (p q : Prop) (r : Type), (q /\ p -> r) -> p -> q -> r 

D'abord, nous nommons tous les lieux:

curry < intros p q r f x y. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Type 
    f : q /\ p -> r 
    x : p 
    y : q 
    ============================ 
    r 

La seule hypothèse qui produit le subgoal r est-f:

curry < apply f. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Type 
    f : q /\ p -> r 
    x : p 
    y : q 
    ============================ 
    q /\ p 

Pour appliquer f nous devons d'abord satisfaire le sous objectifs q et p:

curry < split. 
2 subgoals 

    p : Prop 
    q : Prop 
    r : Type 
    f : q /\ p -> r 
    x : p 
    y : q 
    ============================ 
    q 

subgoal 2 is: 
p 

La prémisse y est une preuve pour subgoal q:

curry < exact y. 
1 subgoal 

    p : Prop 
    q : Prop 
    r : Type 
    f : q /\ p -> r 
    x : p 
    y : q 
    ============================ 
    p 

La prémisse x est une preuve de subgoal p:

curry < exact x. 
No more subgoals. 

Nous en avons terminé . Voici la preuve complète:

curry < Qed. 
intros p q r f x y. 
apply f. 
split. 
exact y. 

exact x. 

curry is defined 

Dans les langages de programmation de fonction comme Haskell vous auriez:

curry :: ((q, p) -> r) -> p -> q -> r 
curry f x y = f (y, x) 

Tout fonctionne en raison de la Curry-Howard correspondence.

Answer 2

Nous avons une preuve Coq grâce à @Aadit, et il serait seulement juste --- éthique? --- de présenter une épreuve Agda.

Une preuve simple et immédiate est

open import Data.Product 

portation : {P Q R : Set} → (P × Q → R) → (P → Q → R) 
portation P×Q→R = λ p q → P×Q→R (p , q) 

Bien sûr, cela ne peut pas du tout être clair si le demandeur ne connaît pas Agda et cherche une formalisation. Alors jetons quelques détails !!

Dans une logique constructive, les propositions peuvent être considérées comme les petits types:

ℙrop = Set 

Alors appairage est la manière habituelle pour former la conjugaison,

data _∧_ (P Q : ℙrop) : Set where 
∧I : P → Q → P ∧ Q 

Dans une logique constructive, l'implication est fonction qui vient d'espace : dire qu'une chose en implique une autre équivaut à produire une procédure qui, avec l'entrée du premier type, renvoie une sortie du second type.L'introduction de l'Implication est alors simplement une définition de fonction habituelle, et l'élimination d'implication n'est alors rien d'autre que l'application de la fonction.

⇒I : ∀ {P Q} → (P → Q) → P ⇒ Q 
⇒I P→Q = P→Q 

⇒E : ∀ {P Q} → P ⇒ Q → P → Q 
⇒E P→Q p = P→Q p 

Maintenant, le demandeur est utilise style déduction naturelle des preuves, donc nous allons introduire un peu de sucre syntaxique pour combler l'écart de la preuve papier et crayon à la formalisation Agda.

syntax ⇒I {P} {Q} (λ p → q) = ⇒-I-assuming-proof p of P we-have Q proved-by q 

Maintenant la preuve!

shunting : (P Q R : ℙrop) → (P ∧ Q) ⇒ R → P ⇒ (Q ⇒ R) 
shunting P Q R P∧Q⇒R = 
        ⇒-I-assuming-proof p of P 
        we-have Q ⇒ R proved-by 

         ⇒-I-assuming-proof q of Q 
         we-have R proved-by 

          ⇒E P∧Q⇒R (∧I p q) 

Ce qui est non seulement assez lisible, mais aussi un peu proche de la présentation du demandeur!

Agda est un tel plaisir!