Suivre

Soumettons cette idée à @MartinShadok car y'a pas que des idées de startup dans la vie, y'a aussi des idées de tactiques Coq.
Imaginons que tu veuilles prouver un truc qui t'arrange, mais tes hypothèses ne te le permettent pas. Avec la tactique BFNTV, tu peux remplacer une hypothèse par une autre de ton choix (par ex. issue du package alternative-facts) et ensuite l'utiliser pour prouver la conclusion qui t'arrange. Ca doit pas être très dur à implémenter, dommage j'y connais rien en Coq.

@oranadoz En vrai, elle serait vachement défouloir à écrire, cette bibliothèque alternative-fact ☺️

On aurait le fameux trumpiste « si on le dit, c'est forcément vrai » de la forme : forall P, looks_stupid P -> P.

On aurait toutes les formes de généralisation abusive : forall P, (exists x, P x) -> forall x, P x.

On aurait la preuve par l'absurde absurde : forall P, ~ ~ ~ P -> P.

Décidément, il y a du potentiel. Si on me pousse à écrire cette bibliothèque, je vais probablement finir par la faire 😂

@MartinShadok Allez, demain c'est dimanche, tu peux le faire 😉

@oranadoz Ĥĥĥĥĥooo. Bon, d’accord ^^
Tu me prends par les sentiments ☺
Donnes moi un jour : github.com/Mbodin/coq-alternat

Inscrivez-vous pour prendre part à la conversation
Framapiaf

Framapiaf est un service de microblog similaire à Twitter. Il est libre, décentralisé et fédéré. Il permet de courts messages (max. 500 caractères), de définir leur degré de confidentialité et de suivre les membres du réseau sans publicité ni pistage.