Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/Rewrite.v

Created August 23, 2024 14:53
Show Gist options
  • Save mukeshtiwari/b40ef742fcd35507b5eb91833e376363 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/b40ef742fcd35507b5eb91833e376363 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Rewrite.v
From Coq Require Import
Program.Tactics
List Psatz.
Program Definition nth_safe {A} (l: list A) (n: nat) (IN: (n < length l)%nat) : A :=
match (nth_error l n) with
| Some res => res
| None => _
end.
Next Obligation.
symmetry in Heq_anonymous. apply nth_error_None in Heq_anonymous. lia.
Defined.
Lemma nth_safe_nth: forall
{A : Type} (l : list A) (n : nat) d
(Ha : (n < length l)), nth_safe l n Ha = nth n l d.
Proof.
intros *.
unfold nth_safe.
pose (fn := (fun (la : list A) (na : nat) (Hb : na < length la)
(o : option A) (Hc : o = nth_error la na) =>
match o as o' return o' = nth_error la na -> A with
| Some res => fun _ : Some res = nth_error la na => res
| None => fun Heq : None = nth_error la na =>
nth_safe_obligation_1 A la na Hb Heq
end Hc) l n Ha).
enough (forall (o : option A) (Ht : o = nth_error l n), fn o Ht = nth n l d) as Htt.
+
eapply Htt.
+
intros *.
destruct o as [x |].
++
simpl.
eapply eq_sym, nth_error_nth; auto.
++
pose proof (proj1(nth_error_None l n) (eq_sym Ht)).
nia.
Qed.
Require Import Lia
Coq.Bool.Bool
Coq.Init.Byte
Coq.NArith.NArith
Coq.Strings.Byte
Coq.ZArith.ZArith
Coq.Lists.List.
Open Scope N_scope.
(* a more complicated definition, for no reason, that I wrote before the simple one *)
Definition np_total (np : N): (np <? 256 = true) -> byte.
Proof.
intros H.
refine(match (np <? 256) as b return forall mp, np = mp ->
(mp <? 256) = b -> _ with
| true => fun mp Hmp Hmpt =>
match of_N mp as npt return _ = npt -> _ with
| Some x => fun _ => x
| None => fun Hf => _
end eq_refl
| false => fun mp Hmp Hmf => _
end np eq_refl eq_refl).
abstract(
apply of_N_None_iff in Hf;
apply N.ltb_lt in Hmpt; nia).
abstract (subst; congruence).
Defined.
(* Now I am trying to prove the same theorem again *)
Lemma np_true : forall np (Ha : np <? 256 = true) x,
of_N np = Some x -> np_total np Ha = x.
Proof.
intros * Hb; unfold np_total.
Fail destruct (np <? 256).
pose (fn := fun (b : bool) (npw : N) (Hw : (npw <? 256) = b)
(f : forall mp : N, npw = mp -> (mp <? 256) = false -> byte) =>
((if b as b' return (forall mp : N, npw = mp -> (mp <? 256) = b' -> byte)
then
(fun
(mp : N) (Hmp : npw = mp) (Hmpt : (mp <? 256) = true) =>
match of_N mp as npt return (of_N mp = npt -> byte) with
| Some x0 => fun _ : of_N mp = Some x0 => x0
| None => fun Hf : of_N mp = None =>
(fun
(npwf mpf : N) (Hmpf : npwf = mpf)
(Hmptf : (mpf <? 256) = true)
(Hff : of_N mpf = None) =>
np_total_subproof npwf mpf Hmpf Hmptf Hff)
npw mp Hmp Hmpt Hf
end eq_refl)
else
(fun (mp : N) (Hmp : npw = mp) (Hmf : (mp <? 256) = false) =>
f mp Hmp Hmf))
npw eq_refl Hw)).
enough (forall b npw H f, b = true -> npw = np -> fn b npw H f = x) as Hc.
+
eapply Hc.
exact Ha. exact eq_refl.
+
intros * Hc Hd.
destruct b; try congruence; subst; simpl.
(* one more generalization *)
clear fn f Hc Ha.
Fail destruct (of_N np).
Check np_total_subproof.
set (fn := (fun (npw : N) (Hc : (npw <? 256) = true)
(o : option byte) (Ha : of_N npw = o) =>
match o as o' return of_N npw = o' -> byte
with
| Some x => fun _ : of_N npw = Some x => x
| None => fun Hf : of_N npw = None =>
np_total_subproof npw npw eq_refl Hc Hf
end Ha) np H).
enough (forall o Hc, o = Some x -> fn o Hc = x) as Hd.
++
eapply Hd.
exact Hb.
++
intros * Hc.
destruct o as [y | ].
+++
simpl; inversion Hc; auto.
+++
congruence.
Qed.
Require Import Coq.Lists.List.
(* Import EqNotations. *)
Definition someListProp (l : list nat) : Prop:=
match nth_error l 10 with
| Some _ => True
| _ => False
end.
Record DepRec := {
l : list nat ;
P : someListProp l
}.
Lemma some_DepRec_lemma (r : DepRec) (f : DepRec -> Prop) : f r.
Proof.
destruct r as [l Hl].
unfold someListProp in *.
Fail destruct ( nth_error l 10).
pose (fn := fun o : option nat => match o with
| Some _ => True
| None => False
end).
pose (o := nth_error l 10).
pose proof (Ha := eq_refl : nth_error l 10 = o).
clearbody o.
Check eq_rect.
pose (Hb := eq_rect _ fn Hl _ Ha).
replace Hl with (eq_rect_r fn Hb Ha) by apply rew_opp_l.
clearbody Hb.
destruct o.
+
unfold fn in Hb.
destruct Hb.
unfold fn.
simpl.
Admitted.
From Coq Require Export RelationClasses Morphisms Setoid.
Class Model :=
{
worlds : Type;
worlds_eq : relation worlds;
worlds_eq_equiv :: Equivalence worlds_eq;
}.
Record state `{Model} :=
{
state_fun : worlds -> bool;
state_proper :: Proper (worlds_eq ==> eq) state_fun
}.
Coercion state_fun : state >-> Funclass. (* Improve readability *)
Context `{Model}.
Context (s : state).
Program Definition restricted_Model `{Model} : Model :=
{|
worlds := {w : worlds | s w = true};
worlds_eq w1 w2 := worlds_eq (proj1_sig w1) (proj1_sig w2)
|}.
Next Obligation.
split.
-
intros []; easy.
-
intros [] []; easy.
-
intros [] [] [] H1 H2;
rewrite H1;
exact H2.
Defined.
Program Definition restricted_state (t : state) : @state restricted_Model :=
{|
state_fun w := t (proj1_sig w)
|}.
Next Obligation.
intros [] [] H3.
rewrite H3.
reflexivity.
Defined.
(*
Theorem gen_goal :
forall (t : state) (w1 w2 : worlds) (sw1 sw2 : bool) (Ha : sw1 = s w1) (Hb : sw2 = s w2),
(if sw1 as anonymous' return (anonymous' = s w1 -> bool)
then fun Heq_anonymous : true = s w1 => t (exist (fun w : worlds => s w = true) w1 (eq_sym Heq_anonymous))
else fun _ : false = s w1 => false) Ha =
(if sw2 as anonymous' return (anonymous' = s w2 -> bool)
then fun Heq_anonymous : true = s w2 => t (exist (fun w : worlds => s w = true) w2 (eq_sym Heq_anonymous))
else fun _ : false = s w2 => false) Hb.
*)
Program Definition unrestricted_state (t : @state restricted_Model) : state :=
{|
state_fun w :=
match s w with
| true => t (exist _ w _)
| false => false
end
|}.
Next Obligation.
intros w1 w2 H1.
unfold unrestricted_state_obligation_1.
pose proof (state_proper s w1 w2 H1) as Hproper.
set (f := fun w (x : bool) =>
(if x as an' return (an' = s w -> bool)
then (fun Heqa => t (exist _ w (eq_sym Heqa))) else fun x => false)).
Check f.
enough (forall sw1 He1 sw2 He2, f w1 sw1 He1 = f w2 sw2 He2) as HH.
1: eapply HH.
intros *.
destruct sw1, sw2.
+
simpl.
apply state_proper.
simpl.
From Coq Require Import Utf8 Psatz.
Section Abs.
Section Moredep.
Set Asymmetric Patterns.
Lemma FnHelper {X Y} (x: X ) {P Q : X -> Y}
(pf : (fun x => P x) = (fun x => Q x)) : P x = Q x.
Proof.
refine(
match pf as pf' in _ = Q' return P x = Q' x with
| eq_refl => eq_refl
end).
Defined.
Section ilist.
Inductive ilist {A : Type} : nat -> Type :=
| Nil : ilist 0
| Cons : A -> forall {n : nat}, ilist n -> ilist (1 + n).
Theorem inversion_ilist_O : forall (A : Type) (ls : @ilist A 0), ls = Nil.
Proof.
intro A.
refine(fix fn ls {struct ls} :=
match ls as ls' in @ilist _ n' return
(forall (pf : n' = 0), ls = @eq_rect _ n' _ ls' 0 pf -> ls = Nil)
with
| Nil => _
| Cons x xs => _
end eq_refl eq_refl).
+
intros * Ha.
admit.
+
intros * Ha.
nia.
Admitted.
(*
Theorem inversion_ilist : forall (A : Type) (n : nat) (ls : @ilist A n),
(n = 0 ∧ ls = Nil) ∨ (exists (m : nat) (x : A) (xs : @ilist A m), n = S m ∧ ls = Cons x xs).
Proof.
intros *.
*)
Theorem subst_one_one {A : Type} : forall (m : nat), 0 = m -> @ilist A m -> @ilist A 0.
Proof.
intros * Ha ls; subst.
exact ls.
Defined.
Theorem subst_one {A : Type} : forall (m : nat) (lsf : ilist m) (pf : 0 = m),
lsf = eq_rect 0 _ Nil m pf ->
@subst_one_one A m pf lsf = eq_rect 0 _ Nil 0 eq_refl.
Proof.
unfold subst_one_one.
intros *. revert lsf.
rewrite <-pf; simpl.
auto.
Qed.
Theorem app {A : Type} {m : nat} (lsf : @ilist A m) :
forall {n : nat}, @ilist A n -> @ilist A (m + n).
Proof.
refine(
(fix fn m lsf {struct lsf} :=
match lsf as lsf' in ilist m'
return forall (pf : m' = m),
lsf = @eq_rect _ m' (fun w => @ilist A w) lsf' m pf ->
forall {n : nat}, ilist n -> ilist (m' + n)
with
| Nil => _
| Cons x xs => _
end eq_refl eq_refl) m lsf).
+
intros * Ha * lss.
(* This manoeuvre is just for
learning *Abstracting over the terms* error and
serves no real purpose in the proof *)
generalize dependent lsf.
rewrite <-pf; intros * Ha.
simpl in Ha.
(*End of manoeuvre*)
exact lss.
+
intros * Ha * lss.
(* This manoeuvre is just for
learning *Abstracting over the terms* error and
serves no real purpose in the proof. *)
generalize dependent lsf.
rewrite <-pf; intros * Ha.
simpl in Ha.
(*End of manoeuvre*)
specialize (fn _ xs _ lss).
exact (Cons x fn).
Defined.
Theorem app_def {A : Type} {m : nat} (lsf : @ilist A m) :
forall {n : nat}, @ilist A n -> @ilist A (m + n).
Proof.
refine
((fix fn m ls {struct ls} :=
match ls in ilist m' return m' = m -> forall {n : nat}, ilist n -> ilist (m' + n)
with
| Nil => _
| Cons x xs => _
end eq_refl) m lsf).
+
intros Ha * lss.
exact lss.
+
intros Ha * lss.
specialize (fn _ xs _ lss).
exact (Cons x fn).
Defined.
End ilist.
End Moredep.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment