mukeshtiwari

From Stdlib Require Import Utf8.

Section Hedberg.
  Context {A : Type} (dec : ∀ x y : A, {x = y} + {x <> y}).

  
  (* Normalise any proof of x = y to the one picked by dec. *)
  #[refine]
  Definition nu {x y : A} (e : x = y) : x = y :=
   match dec x y with 

mukeshtiwari

use curve25519_dalek::ristretto::RistrettoPoint as G;
use group::Group;

use sigma_proofs::composition::{ComposedRelation, ComposedWitness};
use sigma_proofs::traits::{SigmaProtocol, SigmaProtocolSimulator};

mod relations;
pub use relations::*;

fn wrong<R: rand::RngCore + rand::CryptoRng>(n: usize, rng: &mut R) -> Vec<<G as Group>::Scalar> {

mukeshtiwari

In environment
Node : FinType.type
R : BoundedSemiring.type
Hcm : IsCommutativeMonoid.axioms_ R
Hsr : IsSemiring.axioms_ R Hcm
HmulC : ∀ a b : R, a * b = b * a
M : Matrix
H_total_order : ∀ x y : R, x + y = x ∨ x + y = y

mukeshtiwari

From Stdlib Require Import Utf8.


Section Equality.

  (* https://xavierleroy.org/CdF/2018-2019/10.pdf *)
  Definition Leibniz_eq {A : Type} (x y : A) : Prop :=
    ∀ (P : A -> Prop), P x <-> P y.
    
  Theorem Leibniz_equality_forward {A : Type} : 

mukeshtiwari

Section T. 
  
  Variables (A : Type) (B : A -> Type).

  Inductive W : Type := suc : forall (a : A), (B a -> W) -> W.

  Variables (P : W -> Type).
  Fixpoint rec (H : forall a f, (forall b, P (f b)) -> P (suc a f)) (x : W) : P x
    := match x with suc a f => H a f (fun b => rec H (f b)) end.

mukeshtiwari

From Stdlib Require Import 
  Vector Fin Bool Utf8
  Psatz BinIntDef.
Import VectorNotations EqNotations. 


Notation "'existsT' x .. y , p" :=
  (sigT (fun x => .. (sigT (fun y => p)) ..))
    (at level 200, x binder, right associativity,
     format "'[' 'existsT' '/ ' x .. y , '/ ' p ']'") : type_scope.

mukeshtiwari

From Stdlib Require Import Utf8 Fin Psatz List.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin.t n) (g : Fin.t n -> A),
    (forall x, g (f x) = x) ∧ (forall y, f (g y) = y).


Definition bool_to_Fin_2 (x : bool) : Fin.t 2 :=
  if x then Fin.FS Fin.F1 else Fin.F1.

mukeshtiwari

From Stdlib Require Import Utf8 Fin Psatz.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin.t n) (g : Fin.t n -> A),
    (forall x, g (f x) = x) ∧ (forall y, f (g y) = y).


Definition bool_to_Fin_2 (x : bool) : Fin.t 2 :=
  if x then Fin.FS Fin.F1 else Fin.F1.

mukeshtiwari

Section Listmat.

  Context {Node R : Type} 
  (dec_node : forall (c d : Node), {c = d} + {c <> d}).


  Fixpoint cross_product (la lb : list Node) : 
    (list (Node * Node)) :=
    match la with 

mukeshtiwari

import qualified Prelude

__ :: any
__ = Prelude.error "Logical or arity value used"

data Bool =
   True
 | False
 deriving (Prelude.Show)