Skip to content

Instantly share code, notes, and snippets.

View jp-diegidio's full-sized avatar

Julio Di Egidio jp-diegidio

View GitHub Profile
@jp-diegidio
jp-diegidio / NaiveSatSolver.v
Last active December 23, 2023 11:12
Naive SAT solver in Coq
From Coq Require Import Bool.
Ltac solve_sat_naive :=
repeat multimatch goal with
| [|- exists _ : bool, _] => exists true
| [|- exists _ : bool, _] => exists false
end; reflexivity.
Example ex_01 : exists x y, x && negb y = true.
Proof. solve_sat_naive. Qed.
@jp-diegidio
jp-diegidio / prime_gen.pl
Last active November 9, 2023 09:45
Simple prime number generation in Prolog
/*
prime_gen (prime_gen.pl) v1.0.0-rc
Simple prime number generation in Prolog
Copyright (C) 2023 Julio P. Di Egidio
http://julio.diegidio.name
This software is released under the GNU-GPLv3 license.
As usual, NO WARRANTY OF ANY KIND is implied.
*/
@jp-diegidio
jp-diegidio / ExZulip01.v
Last active October 14, 2023 18:03
Exercise Zulip-01 in Coq
(** Exercise Zulip-01
"Prove, by induction on boolean terms, that one step of
evaluation in this lambda calculus reduces the term size."
<https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Tactic.20for.20destructing.20specific.20pattern.20match.20in.20Goal/near/394101120>
*)
Inductive term : Type :=
@jp-diegidio
jp-diegidio / GrellingParadox.v
Last active September 10, 2023 11:55
Grelling–Nelson Paradox (in Coq)
(** Grelling–Nelson Paradox.
Module [GnpLogic] is the basic logical analysis,
with the conclusion "phi is incomplete".
Module [GnpExtLogic] is the first attempt at extending
the logic, but fails to change the conclusion: indeed
it turns out rather indicative that the "paradox" holds
regardless of the specifics of [phi]: having the *type of*
[phi] in the context (IOW, that the class of such functions
@jp-diegidio
jp-diegidio / ilog2.pl
Last active October 27, 2019 19:13
Numerical Snippets in Prolog
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% (SWI-Prolog 7.5.1)
:- module(ilog2,
[ %%
ilog2_n/3, % +X, -Y, -C
ilog2_b/3, % +X, -Y, -C
ilog2_i/3, % +X, -Y, -C
%ilog2_f/3, % +X, -Y, -C
@jp-diegidio
jp-diegidio / WhoOwnsTheFish.pl
Last active October 14, 2023 18:02
Einstein's riddle in Prolog
/*
Einstein's riddle: who owns the fish?
There are 5 houses in 5 different colors in a row. In each house lives a
person with a different nationality. The 5 owners drink a certain type of
beverage, smoke a certain brand of cigar, and keep a certain pet. No
owners have the same pet, smoke the same brand of cigar, or drink the same
beverage. Other facts:
1. The Brit lives in the red house.
@jp-diegidio
jp-diegidio / Nan.Kernel.Ex.pl
Created September 3, 2015 01:51
Answer Sources in Prolog (SWI) - Preview
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/*
Answer Sources in Prolog (SWI) - Preview
Answer Sources: Extensions
Copyright (c) 2015 Julio P. Di Egidio
http://julio.diegidio.name/
All rights reserved.
Answer Sources: Extensions
--------------------------
@jp-diegidio
jp-diegidio / MinimiseCandies.pl
Last active August 29, 2015 14:27
Prolog Puzzles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/*
How few candies does the teacher need?
--------------------------------------
Problem:
Alice is a teacher of kindergarten. She wants to give some candies to
the children in her class. All the children sit in a line and each of
them has a rating score according to his or her usual performance.
@jp-diegidio
jp-diegidio / SudokuSolver.pl
Created April 22, 2015 17:05
Prolog Solvers
% (SWI-Prolog)
:- use_module(library(clpfd)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%! sudoku(?Rows) is nondet.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sudoku(Rows) :-
sudoku__rows(Rows),
sudoku__cols(Rows),
@jp-diegidio
jp-diegidio / DigitProbabilities.pl
Last active November 9, 2023 10:06
Prolog Puzzles
/* ---------------------------------------------------------------------------
How to calculate this probability?
Originally from a question by "Houwu Chen":
https://groups.google.com/d/msg/sci.math/YgvVT-SLvRg/RLn2agzZM7kJ
https://groups.google.com/d/msg/sci.math/YgvVT-SLvRg/2TC-NcV-AqoJ
UPDATED 2015-04-27: Fixed a bug in to_digit_probs__do/4.
Question: