Skip to content

Instantly share code, notes, and snippets.

View mukeshtiwari's full-sized avatar
💭
keep_learning

Mukesh Tiwari mukeshtiwari

💭
keep_learning
129 followers · 1.4k following
View GitHub Profile
@mukeshtiwari
mukeshtiwari / main.ml
Created September 6, 2024 18:39
open Wikimedia
let string_candidates : coq_Node -> string = function
| TC (* Ting Chen (Wing) *) -> "Ting Chen (Wing)"
| SK (* Samuel Klein (Sj) *) -> "Samuel Klein (Sj)"
| KW (* Kat Walsh (mindspillage) *) -> "Kat Walsh (mindspillage)"
| MR (* Milos Rancic (Millosh) *) -> "Milos Rancic (Millosh)"
| LG (* Lodewijk Gelauff (Effeietsanders) *) -> "Lodewijk Gelauff (Effeietsanders)"
| CB (* Claudi Balaguer (Capsot) *) -> "Claudi Balaguer (Capsot)"
@mukeshtiwari
mukeshtiwari / Wikimedia.ml
Created September 6, 2024 18:38
open Mat
open Nat
open Path
type coq_Node =
| TC
| SK
| KW
| MR
| LG
@mukeshtiwari
mukeshtiwari / Mat.ml
Created September 6, 2024 18:37
open Definitions
open List
open Path
(** val get_row : ('a1, 'a2) coq_Matrix -> 'a1 -> 'a1 -> 'a2 **)
let get_row m =
m
(** val get_col : ('a1, 'a2) coq_Matrix -> 'a1 -> 'a1 -> 'a2 **)
@mukeshtiwari
mukeshtiwari / Ceaser.dfy
Created August 24, 2024 07:43
function encode (plain : nat, key : nat) : (out : nat)
requires 0 <= plain < 26
requires 0 <= key < 26
ensures 0 <= out < 26
ensures (plain + key >= 26) ==> out == plain + key - 26
ensures plain + key < 26 ==> out == plain + key
{
if plain + key >= 26 then
plain + key - 26
else
@mukeshtiwari
mukeshtiwari / Fail.v
Created August 23, 2024 17:12
From Coq Require Import
Program.Tactics
List Psatz.
Definition nth_safe {A : Type}
(l : list A) (n : nat) (Ha : (n < length l)) : A.
Proof.
refine
(match (nth_error l n) as nth return (nth_error l n) = nth -> A with
@mukeshtiwari
mukeshtiwari / Beta_expansion.v
Created August 23, 2024 17:01
Require Import Lia
Coq.Bool.Bool
Coq.Init.Byte
Coq.NArith.NArith
Coq.Strings.Byte
Coq.ZArith.ZArith
Coq.Lists.List.
Open Scope N_scope.
@mukeshtiwari
mukeshtiwari / Rewrite.v
Created August 23, 2024 14:53
From Coq Require Import
Program.Tactics
List Psatz.
Program Definition nth_safe {A} (l: list A) (n: nat) (IN: (n < length l)%nat) : A :=
match (nth_error l n) with
| Some res => res
| None => _
end.
@mukeshtiwari
mukeshtiwari / Opamupgrade.text
Created August 11, 2024 18:17
(base) mukesh.tiwari@Mukeshs-MacBook-Pro-2 ~ % opam upgrade
The following actions will be performed:
=== recompile 9 packages
↻ coq-elpi 2.2.3 [uses elpi, ppx_optcomp]
↻ lsp 1.18.0 [uses ppx_yojson_conv_lib]
↻ ocaml-lsp-server 1.18.0~5.2preview [uses base, ppx_yojson_conv_lib]
↻ ocamlformat 0.26.2 [uses ocamlformat-lib]
↻ ocamlformat-lib 0.26.2 [uses base, stdio]
↻ ppx_deriving 6.0.2 [uses ppxlib]
↻ ppx_import 1.11.0 [uses ppxlib]
@mukeshtiwari
mukeshtiwari / Bug.v
Last active May 17, 2024 14:50
CoInductive coAcc {A : Type} (R : A -> A -> Prop) (x : A) : Prop :=
| coAcc_intro : (forall y : A, R x y -> coAcc R y) -> coAcc R x.
CoFixpoint coacc_rect :
forall (A : Type) (R : A -> A -> Prop) (P : A -> Type),
(forall x : A, (forall y : A, R x y -> coAcc R y) ->
(forall y : A, R x y -> P y) -> P x) -> forall x : A, coAcc R x -> P x :=
fun (A : Type) (R : A -> A -> Prop) (P : A -> Type)
(f : (forall x : A, (forall y : A, R x y -> coAcc R y) ->
@mukeshtiwari
mukeshtiwari / the_different_types_of_equality.md
Created May 14, 2024 19:44 — forked from CMCDragonkai/the_different_types_of_equality.md
The Different Types of Equality

The Different Types of Equality

I don't have much to say about this topic since I don't fully understand it.

Basically here are the types of equality I've found:

  • Axiomatic
  • Defined
  • Identity