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.

Follow

@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

Sign in to participate in the conversation
Aleph

Generalistic Mastodon instance for open-minded people. Instance Mastodon généraliste pour personnes ouvertes d'esprit.