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.

· · Web · 1 · 1 · 2

@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 😂

@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

Le réseau social de l'avenir : Pas d'annonces, pas de surveillance institutionnelle, conception éthique et décentralisation ! Possédez vos données avec Mastodon !