mukeshtiwari

Project C is big (4th year project, 3 months full time) and Project B is small (3rd year student, 1 month full time). 

mukeshtiwari

#!/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.

mukeshtiwari

Require Import Field_theory 
  Ring_theory List NArith 
  Ring Field Utf8 Lia Coq.Arith.PeanoNat. 
Import ListNotations.

Section Computation.

  

mukeshtiwari

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

mukeshtiwari

(* 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

mukeshtiwari

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.

mukeshtiwari

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

mukeshtiwari

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.

mukeshtiwari

@[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 
| [], _ => []

mukeshtiwari

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