Skip to content

Instantly share code, notes, and snippets.

View mukeshtiwari's full-sized avatar
💭
keep_learning

Mukesh Tiwari mukeshtiwari

💭
keep_learning
147 followers · 1.4k following
View GitHub Profile
@mukeshtiwari
mukeshtiwari / finitetype.v
Created November 16, 2016 03:16
Theorem indecidable :
forall (b : ballot) (l : list cand),
{forall c : cand, In c l -> b c > 0} + {~ forall c : cand, In c l -> b c > 0}.
Proof.
intros b. induction l.
left; intros. inversion H.
destruct IHl. left; intros.
apply in_inv in H. destruct H.
rewrite <- H. apply g.
@mukeshtiwari
mukeshtiwari / finitetypenew.v
Created November 16, 2016 04:22
Theorem indecidable :
forall (b : ballot) (l : list cand),
{forall c : cand, In c l -> b c > 0} + {~(forall c : cand, In c l -> b c > 0)}.
Proof.
intros b. induction l.
left. intros. inversion H.
destruct IHl. left.
intros c H. apply in_inv in H. destruct H.
admit.
firstorder.
@mukeshtiwari
mukeshtiwari / Omega_solve.v
Created November 18, 2016 05:09
cand : Type
cand_all : list cand
dec_cand : forall n m : cand, {n = m} + {n <> m}
cand_fin : forall c : cand, In c cand_all
wins : cand -> (cand -> cand -> Z) -> Type
loses : cand -> (cand -> cand -> Z) -> Type
is_marg : (cand -> cand -> Z) -> list ballot -> Prop
m : cand -> cand -> Z
p : ballot
c, d : cand
@mukeshtiwari
mukeshtiwari / ceval_deterministic.v
Created December 5, 2016 03:32
Theorem ceval_deterministic: forall (c:com) st st1 st2 s1 s2,
c / st \\ s1 / st1 ->
c / st \\ s2 / st2 ->
st1 = st2 /\ s1 = s2.
Proof.
induction c. intros st st1 st2 s1 s2 H1 H2.
inv H1; inv H2. intuition.
intros. inv H; inv H0. intuition.
intros. inv H; inv H0. intuition.
intros. inv H; inv H0.
@mukeshtiwari
mukeshtiwari / Goals.v
Last active December 5, 2016 04:13
15 subgoals, subgoal 1 (ID 4519)
Inductive ceval : com -> state -> status -> state -> Prop :=
| E_Skip st : CSkip / st \\ SContinue / st
| E_Break st : CBreak / st \\ SBreak / st
| E_Ass st a1 n x : aeval st a1 = n -> (x ::= a1) / st \\ SContinue / (t_update st x n)
| E_IfTrue st st' b c1 c2 s :
beval st b = true -> c1 / st \\ s / st' ->
(IFB b THEN c1 ELSE c2 FI) / st \\ s / st'
| E_IfFalse st st' b c1 c2 s :
beval st b = false -> c2 / st \\ s / st' ->
@mukeshtiwari
mukeshtiwari / IdentityProof.v
Created December 23, 2016 00:06
Fixpoint f_Z_nat (n : Z) : nat :=
match n with
| Z0 => 0
| Zpos p => 2 * Z.to_nat (Zpos p) - 1
| Zneg p => 2 * Z.to_nat (Zpos p)
end.
Eval compute in (f_Z_nat 10).
Eval compute in (f_Z_nat (-2)).
@mukeshtiwari
mukeshtiwari / IntegerNat.v
Last active January 3, 2017 02:53
Fixpoint f_Z_nat (n : Z) : nat :=
match n with
| Z0 => 0
| Zpos p => 2 * Z.to_nat (Zpos p) - 1
| Zneg p => 2 * Z.to_nat (Zpos p)
end.
Eval compute in (f_Z_nat 10).
Eval compute in (f_Z_nat (-2)).
@mukeshtiwari
mukeshtiwari / Maximum of Z
Created January 30, 2017 07:02
Lemma Zmn : forall (m n : Z), m < n -> Z.max m n = n.
@mukeshtiwari
mukeshtiwari / Simplification.v
Created January 30, 2017 23:46
Fixpoint maxlist (l : list Z) : Z :=
match l with
| [] => 0%Z
| [h] => h
| h :: t => Z.max h (maxlist t)
end.
Lemma Max_of_nonempty_list :
@mukeshtiwari
mukeshtiwari / Refine.v
Last active February 3, 2017 04:53
Theorem N : forall (n : nat) (c d : Evote.cand), n <> O -> Z.
refine (fix MM (n : nat) (c d : Evote.cand) := _).
destruct n.
refine (fun H => False_rect _ (H eq_refl)).
refine (fun H => maxlist (map (fun x : Evote.cand => Z.min (Evote.edge c x)
(M n x d)) Evote.cand_all)).
Defined.
(* the function M n maps a pair of candidates c, d to the strength of the strongest path of
length at most (n + 1) *)