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

mukeshtiwari

Lemma fold_left_set_congruence 
  (A : Type) (eqA : brel A)
  (b : binary_op A) (refA : brel_reflexive A eqA)
  (symA : brel_symmetric A eqA) 
  (trnA : brel_transitive A eqA) : 
  ∀ (U V : finite_set A) (a a' : A),
    (eqA a a' = true) -> 
    (brel_set eqA U V = true) ->
    eqA (fold_left b U a) (fold_left b V a') = true.

mukeshtiwari

section Saturday 

  variable 
    {A : Type} 
    [Ord A]

  inductive AAtree : Type 
  | E :  AAtree 
  | T : Nat -> AAtree -> A -> AAtree -> AAtree 
  open AAtree 

mukeshtiwari

P1_P2_commute
	 : ∀ (A P : Type) (zeroP : P) (eqA lteA : brel A) 
         (eqP : brel P) (addP : binary_op P),
         A
         → P
           → ∀ fA : A → A,
               brel_not_trivial A eqA fA
               → brel_congruence A eqA eqA
                 → brel_reflexive A eqA
                   → brel_symmetric A eqA

mukeshtiwari

https://www.kiragoldner.com/blog/job-market.html

mukeshtiwari

(* 
  
  Some lemmas that can be used in conjunction with those in Coq.Lists.List
  
  See https://coq.inria.fr/library/Coq.Lists.List.html
 
 *)

Require Import Lia.
Require Import Coq.Lists.List.

mukeshtiwari

Notation "a =S= b"   := (brel_set  (brel_product eqA eqP) a b = true) (at level 70).
  

  (* = or =S=, both are fine! *)
  Lemma iterate_minset_inv_2 : 
    forall (X W Y : finite_set (A * P)) au bu,
    find (theory.below (manger_pre_order lteA) (au, bu)) X = None -> 
    find (theory.below (manger_pre_order lteA) (au, bu)) Y = None ->
    (* 
    (∀ t : A * P,

mukeshtiwari

Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool 
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.
  
Import Notations ListNotations.

mukeshtiwari

Require Import Coq.Vectors.Vector.
Import VectorNotations.

Fixpoint vappend {T : Type} {n m} (v1 : t T n) (v2 : t T m)
  : t T (plus n m) :=
  match v1 in t _ n return t T (plus n m) with
  | [] => v2
  | x :: v1' => x :: vappend v1' v2
  end.