View Oxford_project.tex
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Project C is big (4th year project, 3 months full time) and Project B is small (3rd year student, 1 month full time). |
View git.migrate
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Field_theory | |
Ring_theory List NArith | |
Ring Field Utf8 Lia Coq.Arith.PeanoNat. | |
Import ListNotations. | |
Section Computation. | |
View Dep_nonsense.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
@[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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
NewerOlder