Mukesh Tiwari mukeshtiwari

💭

keep_learning

Lecturer (Assistant Professor), Swansea University

mukeshtiwari / existential.v

Created October 3, 2016 05:55


	T : Type
	re, re0 : reg_exp T
	Heqre' : Star re0 = Star re
	s1, s2 : list T
	H : s1 =~ re0
	H0 : s2 =~ Star re0
	IHexp_match1 : re0 = Star re ->
	exists ss : list (list T),
	s1 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)

mukeshtiwari / no_idea.v

Created October 3, 2016 06:27

	Lemma MStar'' : forall T (s : list T) (re : reg_exp T),
	s =~ Star re ->
	exists ss : list (list T),
	s = fold app ss []
	/\ forall s', In s' ss -> s' =~ re.
	Proof.
	intros T s re H. remember (Star re) as re'. induction H.
	inversion Heqre'.
	inversion Heqre'.
	inversion Heqre'.

mukeshtiwari / still_no_idea.v

Created October 3, 2016 07:16

	Lemma MStar'' : forall T (s : list T) (re : reg_exp T),
	s =~ Star re ->
	exists ss : list (list T),
	s = fold app ss []
	/\ forall s', In s' ss -> s' =~ re.
	Proof.
	intros T s re H. remember (Star re) as re'. induction H.
	inversion Heqre'.
	inversion Heqre'.
	inversion Heqre'.

mukeshtiwari / congruence.v

Created October 18, 2016 04:26

	Lemma constructive_deci : forall (c d : cand) (k : nat),
	{constructive_prop c d k} + {~(constructive_prop c d k)}.
	Proof.
	intros c d k. unfold constructive_prop.
	remember (all_pairs cand_all) as v.
	destruct (bool_dec ((Fixpoints.iter (O k) (length v) (fun _ => false)) (c, d)) true) as [H \| H].
	left. split. apply path_lfp. unfold Fixpoints.least_fixed_point. unfold Fixpoints.empty_ss.
	rewrite <- Heqv. assumption.
	intros l Hl. apply path_lfp in Hl.
	unfold Fixpoints.least_fixed_point in Hl. unfold Fixpoints.empty_ss in Hl.

mukeshtiwari / s_compile_correct.v

Created October 21, 2016 00:00

	Theorem s_concat_program :
	forall (st : state) (prog1 prog2 : list sinstr) (l : list nat),
	s_execute st l (prog1 ++ prog2) = s_execute st (s_execute st l prog1) prog2.
	Proof.
	intros st. induction prog1.
	auto.
	simpl. intros.
	destruct (s_eval st l a); apply IHprog1.
	Qed.

mukeshtiwari / while_break_true.v

Created October 21, 2016 06:31

	Theorem while_break_true : forall b c st st',
	(WHILE b DO c END) / st \\ SContinue / st' ->
	beval st' b = true ->
	exists st'', c / st'' \\ SBreak / st'.
	Proof.
	intros. remember (WHILE b DO c END) as Hloop.
	induction H; try (inversion HeqHloop); subst.
	congruence. apply IHceval2. auto. auto.
	apply IHceval.

mukeshtiwari / valid_ballot.v

Created October 28, 2016 01:09

	Require Import Coq.ZArith.ZArith. (* integers *)
	Require Import Coq.Lists.List. (* lists *)

	Section Count.

	Variable cand : Type.
	Variable c : cand.
	Variable cand_all : list cand.
	Hypothesis cand_fin : forall c : cand, In c cand_all /\ NoDup cand_all.

mukeshtiwari / ceval_deterministic.v

Created November 2, 2016 02:08

	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.
	inversion H1. inversion H2. intuition. rewrite <- H4.
	rewrite H7. auto.
	intros. inversion H; inversion H0.
	rewrite <- H4. rewrite H7. intuition.

mukeshtiwari / ceval_deterministic.v

Created November 2, 2016 02:42

	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.
	inversion H1. inversion H2. intuition. rewrite <- H4.
	rewrite H7. auto.
	intros. inversion H; inversion H0.
	rewrite <- H4. rewrite H7. intuition.

mukeshtiwari / decidability_ballot.v

Created November 16, 2016 02:17


	Require Import Coq.ZArith.ZArith. (* integers *)
	Require Import Coq.Lists.List. (* lists *)
	Require Import Coq.Lists.ListDec.
	Require Import Notations.
	Require Import Coq.Lists.List.
	Require Import Coq.Arith.Le.
	Require Import Coq.Numbers.Natural.Peano.NPeano.
	Require Import Coq.Arith.Compare_dec.
	Require Import Coq.omega.Omega.