Skip to content

Instantly share code, notes, and snippets.

View mukeshtiwari's full-sized avatar
💭
keep_learning

Mukesh Tiwari mukeshtiwari

💭
keep_learning
View GitHub Profile
View Oxford_project.tex
Project C is big (4th year project, 3 months full time) and Project B is small (3rd year student, 1 month full time).
@mukeshtiwari
mukeshtiwari / git.migrate
Created November 5, 2023 13:35 — forked from niksumeiko/git.migrate
Moving git repository and all its branches, tags to a new remote repository keeping commits history
View git.migrate
#!/bin/bash
# Sometimes you need to move your existing git repository
# to a new remote repository (/new remote origin).
# Here are a simple and quick steps that does exactly this.
#
# Let's assume we call "old repo" the repository you wish
# to move, and "new repo" the one you wish to move to.
#
### Step 1. Make sure you have a local copy of all "old repo"
### branches and tags.
View Ridiculos.v
Require Import Field_theory
Ring_theory List NArith
Ring Field Utf8 Lia Coq.Arith.PeanoNat.
Import ListNotations.
Section Computation.
View Dep_nonsense.v
Require Import List Utf8 Vector Fin Psatz.
Import Notations ListNotations.
Require Import Lia
Coq.Unicode.Utf8
Coq.Bool.Bool
Coq.Init.Byte
Coq.NArith.NArith
Coq.Strings.Byte
Coq.ZArith.ZArith
View Print.v
(* This is with Set Printing All *)
Error: Abstracting over the term "np <? 256" leads to a term
λ b : bool,
∀ f : ∀ mp : N, np = mp → (mp <? 256) = false → byte,
(if b as b0 return (∀ mp : N, np = mp → (mp <? 256) = b0 → byte)
then
λ (mp : N) (Hmp : np = mp) (Hmpt : (mp <? 256) = true),
match of_N mp as npt return (of_N mp = npt → byte) with
| Some x0 => λ _ : of_N mp = Some x0, x0
View Dep_rewrite.v
Require Import List Utf8 Vector Fin Psatz.
Import Notations.
Section Iso.
Definition fin (n : nat) : Type := {i | i < n}.
Theorem fin_to_Fin : ∀ (n : nat), fin n -> Fin.t n.
Proof.
View Twitter.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Parity
import MIL.Common
open Nat List
@[simp]
def fact : Nat -> Nat
| 0 => 1
| n + 1 => (n + 1) * fact n
View Agnishom.v
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Lia.
Require Import Relation_Definitions.
Declare Scope regex_scope.
View List.lean
@[simp]
def take : List Nat -> Nat -> List Nat
| [], _ => []
| _ , 0 => []
| h :: t, (Nat.succ n) => h :: take t n
@[simp]
def drop : List Nat -> Nat -> List Nat
| [], _ => []
View Proof_by_Reflection.txt
https://coq.github.io/doc/V8.11.1/refman/addendum/ring.html
http://poleiro.info/posts/2015-04-13-writing-reflective-tactics.html
https://www.cs.ox.ac.uk/ralf.hinze/publications/TFP09.pdf
https://link.springer.com/chapter/10.1007/978-3-540-30142-4_17
https://dspace.mit.edu/bitstream/handle/1721.1/137403/2018-reification-by-parametricity-itp-draft.pdf?sequence=2&isAllowed=y
https://github.com/coq/coq/blob/v8.18/theories/setoid_ring/Ring_polynom.v
Proving Equalities in a Commutative Ring Done Right in Coq
http://adam.chlipala.net/papers/ReificationITP18/ReificationITP18.pdf
https://github.com/mit-plv/reification-by-parametricity