Preuve ~~ (~~ S -> S) en coq avec seulement des tactiques de base

Question

Est-il possible de résoudre ~~(~~S -> S) en coq? Je sais que vous ne pouvez pas effectuer l'élimination de la double négation dans la logique intuitionniste mais est-ce possible puisque vous démontrez simplement la double négation sur (~~S -> S) par opposition à ~~S -> S lui-même?

Ce n'utilise des tactiques de base et non lemmes de prélude ou bibliothèque standard, etc.

Answer 1

Il est prouvable. Étape par étape, vous le faites comme ceci:

Goal forall S : Prop, ~ ~ (~ ~ S -> S). 
Proof. 
unfold not. 
intros S H1. 
apply H1. 
intro H2. 
apply False_rect. 
apply H2. 
intro H3. 
apply H1. 
intro H4. 
apply H3. 
Defined. 

Ou vous pouvez utiliser tauto, qui est une procédure de décision pour le calcul propositionnel intuitionniste.

Goal forall S : Prop, ~ ~ (~ ~ S -> S). Proof. tauto. Defined.