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.