text:
Require Import Coq.Logic.Decidable.
Require Import SfLib.
Set Implicit Arguments.

Fixpoint lookup_assoc A B (l : list (A * B)) k default (eq_dec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) : B
  := match l with
       | [] => default
       | (k',v)::tl => if (eq_dec k k') then v else lookup_assoc tl k default eq_dec
     end.
Fixpoint update_assoc A B (l : list (A * B)) k v (eq_dec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) : list (A*B)
  := match l with
       | [] => []
       | (k',o)::tl => if (eq_dec k k') then (k',v)::tl else (k',o)::(update_assoc tl k v eq_dec)
     end.
Fixpoint remove_fst A B (x : A) (l : list (A*B)) (eq_dec : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}): list (A*B) :=
    match l with
      | [] => []
      | (y,b)::tl => if (eq_dec x y) then remove_fst x tl eq_dec else (y,b)::(remove_fst x tl eq_dec)
    end.

Lemma in_dec_dec_list :
  (forall A (l1 : list A) l2, (forall a1 a2, In a1 l1 -> In a2 l2 -> a1 = a2 \/ a1 <> a2) -> (l1 = l2 \/ l1 <> l2)).
Proof with eauto.
induction l1. intros. destruct l2; [left; auto | right; congruence].
induction l2. intros. right; congruence. intros. assert (a = a0 \/ a <> a0). apply H; constructor...
assert (l1 = l2 \/ l1 <> l2). apply IHl1. intros. apply H. right... right...
inversion H0; subst.  inversion H1; subst. left; auto. right; congruence. right; congruence.
Qed.

Lemma forall_dec_dec_exists : forall A (P : A -> Prop) (l : list A), (forall a1 a2 : A, a1 = a2 \/ ~ a1 = a2)
  -> Forall (fun e => P e \/ ~ P e) l
  -> decidable (exists e, In e l /\ P e).
Proof with eauto.
intros. unfold decidable in *. induction H0. right; intro. inversion H0. inversion H1. inversion H2.
inversion H0. left. exists x. split... constructor...
inversion IHForall. inversion H3. left; exists x0. inversion H4; split... assert (D := H x x0).
destruct D. subst. contradiction. right. auto.
right. intro. apply H3. inversion H4. exists x0. inversion H5; split... assert (D := H x x0).
destruct D. subst. contradiction. inversion H6. contradiction. auto.
Qed.

Lemma forall_dec_dec_forall : forall A (P : A -> Prop) (l : list A),
  Forall (fun e => P e \/ ~ P e) l -> (Forall P l) \/ ~ (Forall P l).
Proof with eauto.
induction l. intros. left; constructor.
intros. inversion H.
assert (Forall P l \/ ~ Forall P l). apply IHl. apply H3.
inversion H2. inversion H4. left; constructor... right; intro. apply H6. inversion H7...
right. intro. apply H5. inversion H6...
Qed.

Lemma split_components : forall A B (l : list (A*B)), (split l = (fst (split l), snd (split l))).
induction l. reflexivity. remember a as a'; destruct a'; simpl. rewrite IHl. reflexivity.
Qed.

Lemma map_snd_snd_split : forall A B (l : list (A*B)), map (@snd A B) l = snd (split l).
Proof with eauto.
induction l. reflexivity. unfold map. fold (map (@snd A B) l). rewrite IHl.
simpl. remember a as a'; destruct a'. simpl.
rewrite split_components. reflexivity.
Qed.
Lemma map_fst_fst_split : forall A B (l : list (A*B)), map (@fst A B) l =  fst (split l).
Proof with eauto.
induction l. reflexivity. unfold map. fold (map (@fst A B) l). rewrite IHl.
simpl. remember a as a'; destruct a'. simpl.
rewrite split_components. reflexivity.
Qed.

Lemma take_while A (l : list A)
  (P : A -> Prop) (dec : forall x, In x l -> decidable (P x)) :
  (Forall P l) \/ (exists l1 : list A, exists l2 : list A, exists x : A, l = l1 ++ x :: l2 /\ Forall P l1 /\ ~ P x).
Proof with eauto.
  induction l. left; constructor...
  assert (D := forall_dec_dec_forall P (l:=l)).
  assert (Forall P l \/ ~ Forall P l). apply D. unfold decidable in dec. rewrite Forall_forall. intros. apply dec.
  right...
  assert (P a \/ ~ P a). apply dec. left...
  inversion H. inversion H0. left. constructor... right. exists []; exists l; exists a. auto.
  assert (Forall P l \/ exists l1, exists l2, exists x, l = l1 ++ x :: l2 /\ Forall P l1 /\ ~ P x). apply IHl. intros. apply dec.
  right...
  inversion H2. contradiction. clear H2.
  inversion H0. inversion H3. inversion H4. inversion H5. right. exists (a :: x). exists x0. exists x1. inversion H6. split. rewrite H7... inversion H8. split...
  right. exists []; exists l; exists a...
Qed.

Lemma forall_fst_comm : forall A B (l : list (A*B)) (P : A -> Prop),
  Forall (fun ab : A*B => P (fst ab)) l -> Forall P (fst (split l)).
Proof with eauto.
  induction l; intros. constructor. remember a as a'; destruct a'. simpl.
  rewrite (split_components l). simpl. inversion H. constructor. auto. apply IHl. auto.
Qed.
Lemma forall_snd_comm : forall A B (l : list (A*B)) (P : B -> Prop),
  Forall (fun ab : A*B => P (snd ab)) l -> Forall P (snd (split l)).
Proof with eauto.
  induction l; intros. constructor. remember a as a'; destruct a'. simpl.
  rewrite (split_components l). simpl. inversion H. constructor. auto. apply IHl. auto.
Qed.

Lemma fst_split_comm : forall A B l1 (ab : A*B) l2,
  fst (split (l1 ++ ab :: l2)) = fst (split l1) ++ fst ab :: fst (split l2).
Proof with eauto.
  induction l1; intros. destruct ab as (a,b).
  simpl. induction l2; intros. reflexivity.
  destruct a0 as (a0, b0). simpl. rewrite (split_components l2) in *. reflexivity.
  destruct a as (a0, b0). simpl. rewrite (split_components (l1 ++ ab :: l2)). simpl.
  rewrite (split_components l1). simpl. rewrite IHl1. reflexivity.
Qed.
Lemma snd_split_comm : forall A B l1 (ab : A*B) l2,
  snd (split (l1 ++ ab :: l2)) = snd (split l1) ++ snd ab :: snd (split l2).
Proof with eauto.
  induction l1; intros. destruct ab as (a,b).
  simpl. induction l2; intros. reflexivity.
  destruct a0 as (a0, b0). simpl. rewrite (split_components l2) in *. reflexivity.
  destruct a as (a0, b0). simpl. rewrite (split_components (l1 ++ ab :: l2)). simpl.
  rewrite (split_components l1). simpl. rewrite IHl1. reflexivity.
Qed.

Lemma fst_split_cons : forall A B a b (l : list (A*B)), fst (split ((a, b) :: l)) = a :: fst (split l).
  intros. simpl. rewrite (split_components l); simpl. reflexivity.
Qed.
Lemma snd_split_cons : forall A B a b (l : list (A*B)), snd (split ((a, b) :: l)) = b :: snd (split l).
  intros. simpl. rewrite (split_components l); simpl. reflexivity.
Qed.

Lemma fst_split_map_snd : forall A B C (l : list (A*B)) (P : B -> C),
  fst (split (map (fun ab => (fst ab, P (snd ab))) l)) = fst (split l).
Proof with eauto.
  induction l; intros. reflexivity.
  destruct a as (a,b). simpl.
  rewrite (split_components l). rewrite (split_components (map (fun ab => (fst ab, P (snd ab))) l)). simpl.
  f_equal. apply IHl.
Qed.

Lemma snd_split_map_fst : forall A B C (l : list (A*B)) (P : A -> C),
  snd (split (map (fun ab => (P (fst ab), snd ab)) l)) = snd (split l).
Proof with eauto.
  induction l; intros. reflexivity.
  destruct a as (a,b). simpl.
  rewrite (split_components l). rewrite (split_components (map (fun ab => (P (fst ab), snd ab)) l)). simpl.
  f_equal. apply IHl.
Qed.

Lemma forall_app : forall A (l1 : list A) l2 P, Forall P (l1 ++ l2) <-> Forall P l1 /\ Forall P l2.
Proof with eauto.
intros. split. induction l1. simpl... intro. inversion H. split. constructor... apply (IHl1 H3). apply (IHl1 H3).
intros. inversion H. induction l1. simpl... constructor. inversion H0... fold (l1 ++ l2). apply IHl1. split...
inversion H0... inversion H0...
Qed.

Lemma forall_map_comm : forall A B (l : list A) P (f : A -> B), Forall P (map f l) <-> Forall (fun x => P (f x)) l.
Proof with eauto.
  intros; induction l. simpl. split; intros; constructor.
  split. intros. simpl in H. inversion H. constructor... apply IHl...
  intros. inversion H. simpl. constructor... apply IHl...
Qed.

Lemma Forall_in : forall A (l : list A) (P : A -> Prop) e, Forall P l -> In e l -> P e.
Proof with auto.
intros. induction H. inversion H0.
inversion H0. subst. auto. auto.
Qed.

Lemma in_middle : forall A (l1 : list A) e l2, In e (l1 ++ e :: l2).
intros.
induction l1. simpl; left; auto. simpl. right; auto.
Qed.

Lemma remove_fst_in : forall A B (a : A) (b : B) (l : list (A*B)) eq_dec, ~ In (a,b) (remove_fst a l eq_dec).
Proof with eauto.
  induction l. simpl...
  intros. destruct a0 as (xa, xb). simpl. destruct (eq_dec a xa). apply IHl.
  simpl. intro. inversion H. inversion H0. symmetry in H2; contradiction. apply (IHl eq_dec H0).
Qed.
Lemma remove_fst_in_pair : forall A B a (l : list (A*B)) eq_dec, ~ In a (fst (split (remove_fst a l eq_dec))).
Proof with eauto.
  intros. induction l; simpl... intro. apply IHl. destruct a0 as (aa, ab). destruct (eq_dec a aa); simpl...
  simpl in H. rewrite (split_components (remove_fst a l eq_dec)) in H. simpl in H.
  inversion H. symmetry in H0; contradiction. auto.
Qed.
Lemma still_not_in : forall A B s (l:list(A*B)) eq_dec, ~ In s (map (@fst A B) l) -> ~ In s (map (@fst A B) (remove_fst s l eq_dec)).
Proof with auto. induction l; simpl...
  intros; intro. destruct a as (aa, ab). simpl in *.
  assert (aa <> s /\ ~ In s (map (@fst A B) l)). split. intro; apply H; left... intro; apply H; right...
  clear H. inversion_clear H1. destruct (eq_dec s aa). symmetry in e; contradiction.
  inversion H0. simpl in H1; contradiction. unfold not in IHl. apply IHl with eq_dec. intro. contradiction. auto.
Qed.
Theorem in_split_fst : forall A B a (l:list (A*B)), In a (fst (split l)) -> exists l1, exists l2, exists b, l = l1++(a,b)::l2.
Proof.
  induction l; intros; simpl... inversion H. destruct a0 as (xa, xb). rewrite fst_split_cons in H.
  inversion H. exists []; exists l; exists xb... subst; simpl; reflexivity.
  clear H. assert (H := IHl H0). inversion_clear H. inversion_clear H1. inversion_clear H.
  exists ((xa,xb)::x); exists x0; exists x1. subst; simpl. reflexivity.
Qed.

  Lemma remove_app_comm : forall A B l1 (f:A) (x:B) l2 eq_dec,
    remove_fst f (l1 ++ (f, x) :: l2) eq_dec = remove_fst f l1 eq_dec ++ remove_fst f [(f,x)] eq_dec ++ remove_fst f l2 eq_dec.
    Proof with auto. induction l1. simpl... intros. destruct (eq_dec f f)... intros.
      destruct a as (aa, ab). remember ((f, x) :: l2) as temp. simpl.
      destruct (eq_dec f aa). rewrite Heqtemp; apply IHl1. rewrite <- app_comm_cons.
      f_equal. subst. apply IHl1.
    Qed.
Lemma fst_split_comm2 : forall A B (l1 : list(A*B)) l2,
  fst (split (l1 ++ l2)) = fst (split l1) ++ fst (split l2).
Proof with eauto.
  induction l1; intros. simpl...
  simpl.
  destruct a as (a0, b0). rewrite (split_components l1); rewrite (split_components l2);
  rewrite (split_components (l1 ++ l2)); simpl. f_equal...
Qed.
Lemma not_in_remove_eq : forall A B f (l: list (A*B)) eq_dec, ~ In f (fst (split l)) -> l = remove_fst f l eq_dec.
Proof with eauto.
  induction l. intros. simpl...
  intros. destruct a as (s, e). simpl in H. rewrite (split_components l) in H; simpl in H.
  assert (s <> f). intro; apply H; left... assert (~ In f (fst (split l))). intro; apply H; right...
  clear H. assert (H := IHl eq_dec H1). simpl. destruct (eq_dec f s). symmetry in e0; contradiction.
  f_equal...
Qed.
Lemma snd_split_comm2 : forall A B (l1 : list(A*B)) l2,
  snd (split (l1 ++ l2)) = snd (split l1) ++ snd (split l2).
Proof with eauto.
  induction l1; intros. simpl...
  simpl.
  destruct a as (a0, b0). rewrite (split_components l1); rewrite (split_components l2);
  rewrite (split_components (l1 ++ l2)); simpl. f_equal...
Qed.
Lemma update_fieldnames_eq : forall A B (l:list(A*B)) f v eq_dec, map (@fst A B) l = map (@fst A B) (update_assoc l f v eq_dec).
Proof. induction l; intros; auto...
  destruct a as (s,e). simpl. destruct (eq_dec f s); f_equal; simpl. auto. f_equal; apply IHl.
Qed.
Lemma update_values_eq : forall A B l f v P eq_dec, Forall P (map (@snd A B) l) -> P v -> Forall P (map (@snd A B) (update_assoc l f v eq_dec)).
Proof with auto. induction l; intros; simpl; auto. intros.
  destruct a as (s, e). destruct (eq_dec f s). simpl. constructor... inversion H...
  constructor. inversion H... simpl in H. apply IHl. inversion H... auto.
Qed.

author: brownplt

repo: lambdajs-coq

save_path: github-repos/coq/brownplt-lambdajs-coq


text:
Definition subset (A : Type) (u v : A -> Prop) := (forall x : A, u x -> v x).
Definition disjoint (A : Type) (u v : A -> Prop) := forall x, ~ (u x /\ v x).
Definition union (A : Type) (B : (A -> Prop) -> Prop) := fun x : A => exists U, B U /\ U x.
Definition inter (A : Type) (u v : A -> Prop) := fun x : A => u x /\ v x.
Definition empty (A: Type) := fun x : A => False.
Definition full (A: Type) := fun x : A => True.

Structure topology (A : Type) := {
          open :> (A -> Prop) -> Prop;
          empty_open: open (empty _);
          full_open: open (full _);
          inter_open: forall u, open u -> forall v, open v -> open (inter A u v) ;
          union_open: forall s, (subset _ s open) -> open (union A s) }.

(* The discrete topology on a type. *)
Definition discrete (A : Type) : topology A.
Proof.
  exists (full _); firstorder.
Defined.

(* The definition of a T_1 space. *)
Definition T1 {A : Type} (T : topology A) :=
  forall x y : A,
    x <> y ->
      exists u, T u /\ (u x /\ ~ (u y)).

(* The definition of Hausdorff space. *)
Definition hausdorff {A : Type} (T : topology A) :=
  forall x y : A,
  x <> y ->
    exists u, T u /\ exists v, T v /\
      (u x /\ v y /\ disjoint A u v).

(* A discrete space is Hausdorff. *)
Lemma discrete_hausdorff {A : Type} : hausdorff (discrete A).
Proof.
  intros x y N.
  exists (fun z : A => x = z ) ; split ; [exact I | idtac].
  exists (fun z : A => y = z ) ; split ; [exact I | idtac].
  repeat split ; auto.
  intros z [? ?].
  absurd (x = y) ; auto.
  transitivity z ; auto.
Qed.

(* Every Hausdorff space is T1. *)
Lemma hausdorff_is_T1 {A : Type} (T : topology A) :
  hausdorff T -> T1 T.
Proof.
  intros H x y N.
  destruct (H x y N) as [u [? [v [? [? [? G]]]]]].
  exists u ; repeat split ; auto.
  intro.
  absurd (u y /\ v y) ; auto.
Qed.

(* Indiscrete topology. A classical mathematician will be tempted to use
   disjunction: a set is open if it is either empty or the whole set. But
   that relies on excluded middle and generally causes trouble. Here is
   a better definition: a set is open iff as soon as it contains an element,
   it is the whole set. *)
Definition indiscrete (A : Type) : topology A.
Proof.
  exists (fun u : A -> Prop => forall x : A, u x -> (forall y : A, u y) ) ; firstorder.
Defined.

Notation "u <= v" := (subset u v).

(* Let us prove that the indiscrete topology is the least one.
   We seem to need extensionality for propositions. *)
Lemma indiscrete_least (A : Type) (T : topology A) :
  (forall (X : Type) (s t : X -> Prop), (subset _ s t) -> (subset _ t s) -> s = t) ->
  subset _ (indiscrete A) T.
Proof.
  intros ext u H.
  (* Idea: if u is in the indiscrete topology then it is the union of all T-opens v which it meets. *)
  assert (G : (u = union A (fun v : A -> Prop => T v /\ exists x, v x /\ u x ))).
  - apply ext.
    + intros x ?. exists (full _); firstorder using full_open.
    + intros x [v [[? [y [? ?]]] ?]] ; now apply (H y).
  - rewrite G ; apply union_open ; firstorder.
Qed.

(* Particular point topology, see
   http://en.wikipedia.org/wiki/Particular_point_topology, but of course
   without unecessary excluded middle.
*)
Definition particular {A : Type} (x : A) : topology A.
Proof.
  exists (fun u : A -> Prop => (exists y, u y) -> u x ) ; firstorder.
Qed.

(* The topology generated by a family B of subsets that are
   closed under finite intersections. *)

Require Import List.

(* The intersection of a finite list of subsets. *)
Definition inters {A : Type} (us : list (A -> Prop)) : A -> Prop :=
  (fun x : A => Forall (fun u =>  u x) us ).

(* The closure of a family of sets by finite intersections. *)
Definition inter_close {A : Type} (S : (A -> Prop) -> Prop) :=
  (fun v : A -> Prop => exists us, (Forall S) us /\ (forall x, v x <-> inters us x) ).

Lemma Forall_app {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).
Proof.
  induction l1 ; simpl ; auto.
  intros H G.
  constructor.
  - apply (Forall_inv H).
  - apply IHl1 ; auto.
    inversion H ; assumption.
Qed.

Lemma Forall_app1 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P (l1 ++ l2) -> Forall P l1.
Proof.
  induction l1 ; simpl ; auto.
  intro H.
  inversion H ; auto.
Qed.

Lemma Forall_app2 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P (l1 ++ l2) -> Forall P l2.
Proof.
  induction l1 ; simpl ; auto.
  intro H.
  inversion H ; auto.
Qed.

Definition base {A : Type} (B : (A->Prop) -> Prop) :
  B (full _) -> (forall u, B u -> forall v, B v -> B (inter A u v)) -> topology A.
Proof.
  intros H G.
  exists (fun u : A -> Prop => forall x, u x <-> exists v, B v /\ (v x /\ (subset _ v u))).
  - firstorder.
  - firstorder.
  - intros u Hu v Hv x.
    split.
    + intros [Gu Gv].
      destruct (proj1 (Hu x) Gu) as [u' [? [? ?]]].
      destruct (proj1 (Hv x) Gv) as [v' [? [? ?]]].
      exists (inter A u' v') ; firstorder.
    + intros [w [? [? ?]]].
      split ; now apply H2.
  - intros S K x.
    split.
    + intros [u [H1 H2]].
      destruct (K u H1 x) as [L1 _].
      destruct (L1 H2) as [v ?].
      exists v ; firstorder.
    + firstorder.
Defined.

(* The topology generated by a subbase S. *)
Definition subbase {A : Type} (S : (A -> Prop) -> Prop) : topology A.
Proof.
  apply (base (inter_close S)).
  - exists nil ; firstorder using Forall_nil.
  - intros u [us [Hu Gu]] v [vs [Hv Gv]].
    exists (us ++ vs).
    split ; [ (now apply Forall_app) | idtac ].
    split.
    + intros [? ?].
      apply Forall_app ; firstorder.
    + intro K ; split.
      * apply Gu.
        apply (Forall_app1 _ _ _ K).
      * apply Gv.
        apply (Forall_app2 _ _ _ K).
Defined.

(* A subbasic set is open. *)
Lemma subbase_open {A : Type} (S : (A -> Prop) -> Prop) (u : A -> Prop) :
  S u -> (subbase S) u.
Proof.
  intros H x.
  split.
  - intro G.
    exists u ; split ; [ idtac | firstorder ].
    exists (u :: nil).
    split ; [now constructor | idtac].
    intro y ; split.
    + intro ; now constructor.
    + intro K.
      inversion K ; auto.
  - firstorder.
Qed.

(* The cofinite topology on A. *)
Definition cofinite (A : Type) : topology A :=
  subbase (fun u : A -> Prop => exists x, forall y, (u y <-> y <> x) ).

(* The cofinite topology is T1. *)
Lemma cofinite_T1 (A : Type) : T1 (cofinite A).
Proof.
  intros x y N.
  exists (fun z : A => z <> y ).
  split ; auto.
  apply subbase_open.
   exists y ; firstorder.
Qed.

repo: topology


text:
Require Import Unicode.Utf8.
Require Import Game.Mynat.Definition.
Require Import Game.Mynat.Add.
Require Import Game.Mynat.Mul.
Require Import Game.Mynat.Le.
Require Import Game.World.Addition.
Require Import Game.World.Multiplication.
Require Import Game.World.Proposition.
Require Import Game.World.AdvancedProposition.
Require Import Game.World.AdvancedAddition.
Require Import Game.World.AdvancedMultiplication.

(* Level 1 *)
(* `exists x`: Replace existentially quantified variable with `x` *)
(* Goal of the form `∃ y, ... ` *)

Lemma one_add_le_self (x : mynat) : x ≤ 1 + x.
Proof.
  rewrite le_iff_exists_add.
  exists 1.
  exact (add_comm 1 x).
Qed.

(* Level 2 *)

Lemma le_refl (x : mynat) : x ≤ x.
Proof.
  exists 0.
  reflexivity.
Qed.

(* Level 3 *)
(* `destruct f as [x g]`: Replace existentially quantified variable in hypothesis `f` with `x` *)
(* Hypothesis of the form `f: ∃ y, ...` *)

Theorem le_succ (a b : mynat) : a ≤ b → a ≤ (succ b).
Proof.
  intro f.
  destruct f as [c g].
  exists (succ c).
  rewrite add_succ.
  rewrite succ_eq_succ_iff.
  exact g.
Qed.

(* Level 4 *)

Lemma zero_le (a : mynat) : 0 ≤ a.
Proof.
  exists a.
  rewrite zero_add.
  reflexivity.
Qed.

(* Level 5 *)

Theorem le_trans (a b c : mynat) (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c.
Proof.
  destruct hab as [d hab].
  destruct hbc as [e hbc].
  rewrite hab in hbc.
  exists (d + e).
  rewrite <- add_assoc.
  exact hbc.
Qed.

(* Level 6 *)

Theorem le_antisymm (a b : mynat) (hab : a ≤ b) (hba : b ≤ a) : a = b.
Proof.
  destruct hab as [c hab].
  destruct hba as [d hba].
  rewrite hab in hba.
  rewrite add_assoc in hba.
  symmetry in hba.
  apply eq_zero_of_add_right_eq_self in hba.
  rewrite add_comm in hba.
  apply add_left_eq_zero in hba.
  rewrite hba in hab.
  symmetry in hab.
  exact hab.
Qed.

(* Level 7 *)

Lemma le_zero (a : mynat) (h : a ≤ 0) : a = 0.
Proof.
  destruct h as [c h].
  symmetry in h.
  exact (add_right_eq_zero h).
Qed.

(* Level 8 *)

Lemma succ_le_succ (a b : mynat) (h : a ≤ b) : succ a ≤ succ b.
Proof.
  destruct h as [c h].
  exists c.
  rewrite succ_add.
  rewrite succ_eq_succ_iff.
  exact h.
Qed.

(* Level 9 *)

Theorem le_total (a b : mynat) : a ≤ b ∨ b ≤ a.
Proof.
  induction a.
  left.
  exact (zero_le b).
  destruct IHa as [f|g].
  destruct f as [c f].
  destruct c.
  right.
  exists 1.
  rewrite f.
  reflexivity.
  left.
  rewrite f.
  exists c.
  rewrite add_succ.
  rewrite succ_add.
  reflexivity.
  right.
  apply le_succ.
  exact g.
Qed.

(* Level 10 *)

Lemma le_succ_self (a : mynat) : a ≤ succ a.
Proof.
  exact (le_succ a a (le_refl a)).
Qed.

(* Level 11 *)

Theorem add_le_add_right {a b : mynat} : a ≤ b → ∀ t, (a + t) ≤ (b + t).
Proof.
  intro f.
  intro t.
  destruct f as [c f].
  exists c.
  rewrite add_right_comm.
  rewrite add_right_cancel_iff.
  exact f.
Qed.

(* Level 12 *)

Theorem le_of_succ_le_succ (a b : mynat) : succ a ≤ succ b → a ≤ b.
Proof.
  intro f.
  destruct f as [c f].
  exists c.
  rewrite succ_add in f.
  rewrite succ_eq_succ_iff in f.
  exact f.
Qed.

(* Level 13 *)

Theorem not_succ_le_self (a : mynat) : ¬ (succ a ≤ a).
Proof.
  intro f.
  pose (g := le_antisymm a (succ a) (le_succ_self a)).
  apply g in f.
  apply (ne_succ_self a).
  exact f.
Qed.

(* Level 14 *)

Theorem add_le_add_left {a b : mynat} (h : a ≤ b) (t : mynat) :
  t + a ≤ t + b.
Proof.
  rewrite add_comm.
  rewrite (add_comm t b).
  apply add_le_add_right.
  exact h.
Qed.

(* Level 15 *)

Lemma lt_aux_one (a b : mynat) : a ≤ b ∧ ¬ (b ≤ a) → succ a ≤ b.
Proof.
  intro f.
  destruct f as [f g].
  destruct f as [c f].
  destruct c.
  exfalso.
  apply g.
  exists 0.
  rewrite f.
  reflexivity.
  exists c.
  rewrite succ_add.
  rewrite add_succ in f.
  exact f.
Qed.

(* Level 16 *)

Lemma lt_aux_two (a b : mynat) : succ a ≤ b → a ≤ b ∧ ¬ (b ≤ a).
Proof.
  intro f.
  split.
  destruct f as [c f].
  exists (1 + c).
  rewrite <- add_assoc.
  exact f.
  intro g.
  pose (h := le_trans (succ a) b a f g).
  exact (not_succ_le_self a h).
Qed.

(* Level 17 *)

Lemma lt_iff_succ_le (a b : mynat) : a < b ↔ succ a ≤ b.
Proof.
  split.
  exact (lt_aux_one a b).
  exact (lt_aux_two a b).
Qed.

author: uncomputable

repo: natural-number-game


text:
From isla Require Import opsem.

Definition instr_stp : isla_trace :=
  AssumeReg "HCR_EL2" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t:
  AssumeReg "CFG_ID_AA64PFR0_EL1_EL3" [] (RegVal_Base (Val_Bits (BV 4%N 0x1%Z))) Mk_annot :t:
  AssumeReg "CFG_ID_AA64PFR0_EL1_EL2" [] (RegVal_Base (Val_Bits (BV 4%N 0x1%Z))) Mk_annot :t:
  AssumeReg "CFG_ID_AA64PFR0_EL1_EL1" [] (RegVal_Base (Val_Bits (BV 4%N 0x1%Z))) Mk_annot :t:
  AssumeReg "CFG_ID_AA64PFR0_EL1_EL0" [] (RegVal_Base (Val_Bits (BV 4%N 0x1%Z))) Mk_annot :t:
  AssumeReg "TCR_EL2" [] (RegVal_Base (Val_Bits (BV 64%N 0x0%Z))) Mk_annot :t:
  AssumeReg "EDSCR" [] (RegVal_Base (Val_Bits (BV 32%N 0x0%Z))) Mk_annot :t:
  AssumeReg "OSDLR_EL1" [] (RegVal_Base (Val_Bits (BV 32%N 0x0%Z))) Mk_annot :t:
  AssumeReg "OSLSR_EL1" [] (RegVal_Base (Val_Bits (BV 32%N 0x0%Z))) Mk_annot :t:
  Smt (DeclareConst 6%Z (Ty_BitVec 1%N)) Mk_annot :t:
  AssumeReg "PSTATE" [Field "EL"] (RegVal_Base (Val_Bits (BV 2%N 0x2%Z))) Mk_annot :t:
  AssumeReg "PSTATE" [Field "SP"] (RegVal_Base (Val_Bits (BV 1%N 0x1%Z))) Mk_annot :t:
  AssumeReg "PSTATE" [Field "nRW"] (RegVal_Base (Val_Bits (BV 1%N 0x0%Z))) Mk_annot :t:
  AssumeReg "SCR_EL3" [] (RegVal_Base (Val_Bits (BV 32%N 0x501%Z))) Mk_annot :t:
  AssumeReg "SCTLR_EL2" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000002%Z))) Mk_annot :t:
  Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t:
  Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "SP_EL2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0xfff0000000000007%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
  Assume (AExp_Binop ((Bvcomp Bvugt)) (AExp_Val (AVal_Var "SP_EL2" []) Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x10%Z)) Mk_annot) Mk_annot) Mk_annot :t:
  ReadReg "SP_EL2" [] (RegVal_Base (Val_Symbolic 29%Z)) Mk_annot :t:
  Smt (DefineConst 73%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 29%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffff0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
  Smt (DeclareConst 74%Z (Ty_BitVec 64%N)) Mk_annot :t:
  ReadReg "R0" [] (RegVal_Base (Val_Symbolic 74%Z)) Mk_annot :t:
  Smt (DefineConst 75%Z (Val (Val_Symbolic 74%Z) Mk_annot)) Mk_annot :t:
  Smt (DeclareConst 76%Z (Ty_BitVec 64%N)) Mk_annot :t:
  ReadReg "R1" [] (RegVal_Base (Val_Symbolic 76%Z)) Mk_annot :t:
  Smt (DefineConst 77%Z (Val (Val_Symbolic 76%Z) Mk_annot)) Mk_annot :t:
  Smt (DefineConst 78%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 73%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
  Smt (DefineConst 83%Z (Binop (Eq) (Val (Val_Symbolic 78%Z) Mk_annot) (Manyop (Bvmanyarith Bvand) [Val (Val_Symbolic 78%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffff8%Z)) Mk_annot] Mk_annot) Mk_annot)) Mk_annot :t:
  ReadReg "PSTATE" [Field "D"] (RegVal_Struct [("D", RegVal_Base (Val_Symbolic 6%Z))]) Mk_annot :t:
  Smt (DeclareConst 2117%Z (Ty_BitVec 64%N)) Mk_annot :t:
  ReadReg "MPIDR_EL1" [] (RegVal_Base (Val_Symbolic 2117%Z)) Mk_annot :t:
  Smt (DeclareConst 2300%Z (Ty_BitVec 56%N)) Mk_annot :t:
  Smt (DefineConst 2313%Z (Unop (ZeroExtend 8%N) (Manyop Concat [Val (Val_Bits (BV 4%N 0x0%Z)) Mk_annot; Unop (Extract 51%N 0%N) (Val (Val_Symbolic 78%Z) Mk_annot) Mk_annot] Mk_annot) Mk_annot)) Mk_annot :t:
  Smt (DeclareConst 2314%Z Ty_Bool) Mk_annot :t:
  WriteMem (RegVal_Base (Val_Symbolic 2314%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 6%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 2313%Z)) (RegVal_Base (Val_Symbolic 75%Z)) 8%N None Mk_annot :t:
  Smt (DefineConst 2315%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 73%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
  Smt (DefineConst 2320%Z (Binop (Eq) (Val (Val_Symbolic 2315%Z) Mk_annot) (Manyop (Bvmanyarith Bvand) [Val (Val_Symbolic 2315%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xfffffffffffffff8%Z)) Mk_annot] Mk_annot) Mk_annot)) Mk_annot :t:
  Smt (DefineConst 4515%Z (Unop (ZeroExtend 8%N) (Manyop Concat [Val (Val_Bits (BV 4%N 0x0%Z)) Mk_annot; Unop (Extract 51%N 0%N) (Val (Val_Symbolic 2315%Z) Mk_annot) Mk_annot] Mk_annot) Mk_annot)) Mk_annot :t:
  Smt (DeclareConst 4516%Z Ty_Bool) Mk_annot :t:
  WriteMem (RegVal_Base (Val_Symbolic 4516%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 6%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 4515%Z)) (RegVal_Base (Val_Symbolic 77%Z)) 8%N None Mk_annot :t:
  Smt (DefineConst 4517%Z (Val (Val_Symbolic 73%Z) Mk_annot)) Mk_annot :t:
  WriteReg "SP_EL2" [] (RegVal_Base (Val_Symbolic 4517%Z)) Mk_annot :t:
  Smt (DeclareConst 4518%Z (Ty_BitVec 64%N)) Mk_annot :t:
  ReadReg "_PC" [] (RegVal_Base (Val_Symbolic 4518%Z)) Mk_annot :t:
  Smt (DefineConst 4519%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4518%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
  WriteReg "_PC" [] (RegVal_Base (Val_Symbolic 4519%Z)) Mk_annot :t:
  tnil
.

author: rems-project

repo: islaris

save_path: github-repos/coq/rems-project-islaris


text:
Require Import GhostSimulations.

Require Import Raft.
Require Import CommonTheorems.
Require Import SpecLemmas.
Require Import RaftMsgRefinementInterface.

Require Import NextIndexSafetyInterface.
Require Import RefinedLogMatchingLemmasInterface.

Require Import UpdateLemmas.
Local Arguments update {_} {_} {_} _ _ _ _ : simpl never.
Require Import GhostLogCorrectInterface.

Section GhostLogCorrectProof.
  Context {orig_base_params : BaseParams}.
  Context {one_node_params : OneNodeParams orig_base_params}.
  Context {raft_params : RaftParams orig_base_params}.

  Context {rmri : raft_msg_refinement_interface}.
  Context {nisi : nextIndex_safety_interface}.
  Context {rlmli : refined_log_matching_lemmas_interface}.

  Ltac update_destruct :=
    match goal with
      | [ |- context [ update _ ?y _ ?x ] ] => destruct (name_eq_dec y x)
    end.

  Ltac update_destruct_hyp :=
    match goal with
      | [ _ : context [ update _ ?y _ ?x ] |- _ ] => destruct (name_eq_dec y x)
    end.

  Ltac destruct_update :=
    repeat (first [update_destruct_hyp|update_destruct]; subst; rewrite_update).

  Definition lifted_nextIndex_safety net : Prop :=
    forall h h',
      type (snd (nwState net h)) = Leader ->
      pred (getNextIndex (snd (nwState net h)) h') <= maxIndex (log (snd (nwState net h))).

  Lemma lifted_nextIndex_safety_invariant :
    forall (net : @network _ raft_msg_refined_multi_params),
      msg_refined_raft_intermediate_reachable net ->
      lifted_nextIndex_safety net.
  Proof using nisi rmri.
    intros.
    enough (nextIndex_safety (deghost (mgv_deghost net))) by
        (unfold nextIndex_safety, lifted_nextIndex_safety, deghost, mgv_deghost in *;
         simpl in *;
         repeat break_match; simpl in *; auto).
    apply msg_lift_prop_all_the_way; eauto using nextIndex_safety_invariant.
  Qed.

  Definition lifted_entries_contiguous net :=
    forall h,
      contiguous_range_exact_lo (log (snd (nwState net h))) 0.

  Definition lifted_entries_sorted net :=
    forall h,
      sorted (log (snd (nwState net h))).

  Lemma lifted_entries_contiguous_invariant :
    forall (net : @network _ raft_msg_refined_multi_params),
      msg_refined_raft_intermediate_reachable net ->
      lifted_entries_contiguous net.
  Proof using rlmli rmri.
    intros.
    enough (entries_contiguous (mgv_deghost net)) by
        (unfold entries_contiguous, lifted_entries_contiguous, mgv_deghost in *;
         simpl in *;
         repeat break_match; simpl in *; auto).
    apply msg_lift_prop; eauto using entries_contiguous_invariant.
  Qed.

  Lemma lifted_entries_sorted_invariant :
    forall (net : @network _ raft_msg_refined_multi_params),
      msg_refined_raft_intermediate_reachable net ->
      lifted_entries_sorted net.
  Proof using rlmli rmri.
    intros.
    enough (entries_sorted (mgv_deghost net)) by
        (unfold entries_sorted, lifted_entries_sorted, mgv_deghost in *;
         simpl in *;
         repeat break_match; simpl in *; auto).
    apply msg_lift_prop; eauto using entries_sorted_invariant.
  Qed.

  Lemma ghost_log_correct_append_entries :
    msg_refined_raft_net_invariant_append_entries ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    find_apply_hyp_hyp; intuition; eauto.
    subst. simpl in *.
    subst.
    find_apply_lem_hyp handleAppendEntries_not_append_entries.
    intuition. find_false.
    repeat eexists; eauto.
  Qed.

  Lemma ghost_log_correct_append_entries_reply :
    msg_refined_raft_net_invariant_append_entries_reply ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    find_apply_hyp_hyp; intuition; eauto.
    subst. simpl in *.
    subst.
    find_apply_lem_hyp handleAppendEntriesReply_packets.
    subst. simpl in *. intuition.
  Qed.

  Lemma ghost_log_correct_request_vote :
    msg_refined_raft_net_invariant_request_vote ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    find_apply_hyp_hyp; intuition; eauto.
    subst. simpl in *.
    subst.
    find_apply_lem_hyp handleRequestVote_no_append_entries.
    intuition. find_false.
    repeat eexists; eauto.
  Qed.

  Lemma ghost_log_correct_request_vote_reply :
    msg_refined_raft_net_invariant_request_vote_reply ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    find_apply_hyp_hyp; intuition; eauto.
  Qed.

  Lemma doLeader_replicaMessage :
    forall h st os st' ms m,
      doLeader st h = (os, st', ms) ->
      In m ms ->
      type st = Leader /\
      exists h',
        m = replicaMessage st' h h'.
  Proof using.
    unfold doLeader in *.
    intros; repeat break_match; find_inversion; simpl in *; intuition.
    do_in_map. eauto.
  Qed.

  Lemma doLeader_getNextIndex :
    forall h h' st os st' ms,
      doLeader st h = (os, st', ms) ->
      getNextIndex st' h' = getNextIndex st h'.
  Proof using.
    intros.
    unfold getNextIndex, doLeader, advanceCommitIndex in *.
    repeat break_match; find_inversion; simpl in *; auto.
  Qed.

  Lemma ghost_log_correct_do_leader :
    msg_refined_raft_net_invariant_do_leader ghost_log_correct.
  Proof using rlmli nisi rmri.
    red. unfold ghost_log_correct. intros. simpl in *.
    match goal with
      | H : nwState ?net ?h = (?gd, ?d) |- _ =>
        replace gd with (fst (nwState net h)) in * by (rewrite H; reflexivity);
          replace d with (snd (nwState net h)) in * by (rewrite H; reflexivity);
          clear H
    end.
    find_apply_hyp_hyp; intuition; eauto.
    do_in_map.
    subst. simpl in *.
    unfold add_ghost_msg in *. do_in_map. subst. simpl in *.
    find_eapply_lem_hyp doLeader_replicaMessage; eauto.
    break_and.
    break_exists. subst.
    unfold replicaMessage in *.
    simpl in *. find_inversion.
    unfold write_ghost_log. simpl.
    match goal with
      | |- context [pred ?x] =>
        remember (pred x) as index
    end.
    destruct index.
    - left. intuition; eauto.
      + break_match; intuition.
        find_apply_lem_hyp findAtIndex_elim.
        intuition.
        find_erewrite_lem doLeader_log; eauto.
        enough (0 < eIndex e) by omega.
        eapply lifted_entries_contiguous_invariant; eauto.
      + erewrite doLeader_log; eauto.
        apply sorted_findGtIndex_0; [|eapply lifted_entries_sorted_invariant; eauto].
        intros. eapply lifted_entries_contiguous_invariant; eauto.
    - right.
      erewrite doLeader_log; eauto.
      enough (exists e, findAtIndex (log (snd (nwState net leaderId))) (S index) = Some e) by
          (break_exists_name e;
           find_copy_apply_lem_hyp findAtIndex_elim; intuition;
           auto;
           exists e; intuition;
             do 2 (unfold raft_data in *; simpl in *);
             repeat find_rewrite; auto).
      eapply contiguous_findAtIndex;
        [eapply lifted_entries_sorted_invariant; eauto|
         eapply lifted_entries_contiguous_invariant; eauto|].
      intuition.
      repeat find_rewrite.
      erewrite doLeader_getNextIndex; eauto.
      eapply lifted_nextIndex_safety_invariant; eauto.
  Qed.

  Lemma ghost_log_correct_do_generic_server :
    msg_refined_raft_net_invariant_do_generic_server ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    match goal with
      | H : nwState ?net ?h = (?gd, ?d) |- _ =>
        replace gd with (fst (nwState net h)) in * by (rewrite H; reflexivity);
          replace d with (snd (nwState net h)) in * by (rewrite H; reflexivity);
          clear H
    end.
    find_apply_hyp_hyp; intuition; eauto.
    find_apply_lem_hyp doGenericServer_packets.
    subst. simpl in *. intuition.
  Qed.

  Lemma ghost_log_correct_reboot :
    msg_refined_raft_net_invariant_reboot ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    match goal with
      | H : nwState ?net ?h = (?gd, ?d) |- _ =>
        replace gd with (fst (nwState net h)) in * by (rewrite H; reflexivity);
          replace d with (snd (nwState net h)) in * by (rewrite H; reflexivity);
          clear H
    end.
    repeat find_reverse_rewrite. eauto.
  Qed.

  Lemma ghost_log_correct_client_request :
    msg_refined_raft_net_invariant_client_request ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    find_apply_hyp_hyp; intuition; eauto.
    subst. simpl in *.
    subst.
    find_apply_lem_hyp handleClientRequest_packets.
    subst. simpl in *. intuition.
  Qed.

  Lemma ghost_log_correct_timeout :
    msg_refined_raft_net_invariant_timeout ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    find_apply_hyp_hyp; intuition; eauto.
    exfalso.
    subst. simpl in *.
    subst. do_in_map. subst.
    simpl in *. unfold add_ghost_msg in *.
    do_in_map. subst. simpl in *.
    find_eapply_lem_hyp handleTimeout_packets; eauto.
    repeat find_rewrite. intuition. find_false.
    repeat eexists; eauto.
  Qed.

  Lemma ghost_log_correct_state_same_packet_subset :
    msg_refined_raft_net_invariant_state_same_packet_subset ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    eauto.
  Qed.

  Lemma ghost_log_correct_init :
    msg_refined_raft_net_invariant_init ghost_log_correct.
  Proof using.
    red. unfold ghost_log_correct. intros. simpl in *.
    intuition.
  Qed.

  Instance glci : ghost_log_correct_interface.
  Proof.
    split. intros.
    apply msg_refined_raft_net_invariant; auto.
    - apply ghost_log_correct_init.
    - apply ghost_log_correct_client_request.
    - apply ghost_log_correct_timeout.
    - apply ghost_log_correct_append_entries.
    - apply ghost_log_correct_append_entries_reply.
    - apply ghost_log_correct_request_vote.
    - apply ghost_log_correct_request_vote_reply.
    - apply ghost_log_correct_do_leader.
    - apply ghost_log_correct_do_generic_server.
    - apply ghost_log_correct_state_same_packet_subset.
    - apply ghost_log_correct_reboot.
  Qed.

End GhostLogCorrectProof.

author: ahmet-celik

repo: pverdi

save_path: github-repos/coq/ahmet-celik-pverdi


text:
Load LFindLoad.
Load LFindLoad.
From adtind Require Import goal13.

From lfind Require Import LFind.
Require Import Extraction.
Extract Inductive nat => nat [ "(O)" "S" ].
Extract Inductive list => list [ "Nil" "Cons" ].
Extraction "/home/yousef/lemmafinder/benchmark/_lfind_clam_lf_goal13_theorem0_36_lem/goal13_lfind_orig.ml"  adtind.goal13.plus adtind.goal13.half.
Success.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Set Implicit Arguments.

Require Import Bedrock.Platform.Cito.Wf.
Export Wf.

Section TopSection.

  Require Import Bedrock.Platform.Cito.SyntaxFunc.
  Require Bedrock.Platform.Cito.CompileStmtSpec.
  Require Import Bedrock.Platform.Cito.GetLocalVars.
  Require Import Bedrock.Platform.Cito.Depth.
  Require Import Bedrock.Platform.Cito.WellFormed.
  Require Import Bedrock.Platform.Cito.ListFacts3.

  Definition GoodFunc f :=
    let body := Body f in
    let local_vars := get_local_vars body (ArgVars f) (RetVar f) in
    is_no_dup (ArgVars f) = true /\
    NoUninitialized (ArgVars f) (RetVar f) body /\
    wellformed body /\
    goodSize (length local_vars + depth body).

  Hint Constructors NoDup.

  Require Import Bedrock.Platform.Cito.GeneralTactics.
  Require Import Bedrock.Platform.Cito.GetLocalVarsFacts.

  Lemma GoodFunc_syn_req :
    forall f,
      GoodFunc f ->
      let body := Body f in
      let local_vars := get_local_vars body (ArgVars f) (RetVar f) in
      let all_vars := ArgVars f ++ local_vars in
      CompileStmtSpec.syn_req all_vars (depth body) body.
    simpl; intros.
    unfold CompileStmtSpec.syn_req.
    destruct H; openhyp.
    split; eauto.
    unfold CompileStmtSpec.in_scope.
    split; eauto.
    eapply get_local_vars_subset; eauto.
  Qed.

  Lemma NoDup_app : forall A (ls2 ls1 : list A),
    NoDup ls1
    -> NoDup ls2
    -> (forall x, In x ls1 -> ~In x ls2)
    -> NoDup (ls1 ++ ls2).
    induction 1; simpl; intuition.
    constructor; auto.
    intro.
    apply in_app_or in H4; intuition eauto.
    eauto.
  Qed.

  Lemma In_InA : forall A (x : A) ls,
    List.In x ls
    -> SetoidList.InA (@Logic.eq A) x ls.
    induction ls; simpl; intuition.
  Qed.

  Lemma NoDupA_NoDup : forall A ls,
    SetoidList.NoDupA (@Logic.eq A) ls
    -> List.NoDup ls.
    induction 1; intuition auto using In_InA.
  Qed.

  Require Import Bedrock.Platform.Cito.GetLocalVars.
  Require Import Bedrock.Platform.Cito.GeneralTactics2.
  Require Import Bedrock.Platform.Cito.SetoidListFacts.
  Require Import Bedrock.Platform.Cito.GeneralTactics.
  Require Import Bedrock.Platform.Cito.StringSetFacts.
  Lemma GoodFunc_NoDup_vars : forall f, GoodFunc f -> forall s r, NoDup (ArgVars f ++ get_local_vars s (ArgVars f) r).
    unfold GoodFunc; intuition.
    apply NoDup_app; auto.
    {
      eapply is_no_dup_sound; eauto.
    }
    {
      apply NoDupA_NoDup.
      apply StringSet.StringSet.elements_3w.
    }
    intros.
    nintro.
    unfold get_local_vars in H4.
    eapply InA_eq_In_iff in H4.
    eapply StringSet.StringSet.elements_2 in H4.
    eapply StringSet.StringFacts.diff_iff in H4.
    openhyp.
    contradict H5.
    eapply of_list_spec; eauto.
  Qed.

End TopSection.

Require Import Bedrock.Platform.Cito.ADT.

Module Make (Import E : ADT).

  Module Import WfMake := Wf.Make E.
  Require Import Bedrock.Platform.Cito.Semantics.
  Import SemanticsMake.

  Require Import Bedrock.Platform.Cito.GeneralTactics.

  Section TopSection.

    Lemma GoodFunc_Safe : forall f, GoodFunc f -> let s := Body f in forall fs vs h, Safe fs s (vs, h) -> forall vs', agree_in vs vs' (ArgVars f) -> Safe fs s (vs', h).
      intros.
      eapply NoUninitialized_Safe; eauto.
      destruct H; openhyp; eauto.
    Qed.

    Lemma GoodFunc_RunsTo : forall f, GoodFunc f -> let s := Body f in forall fs vs h v', RunsTo fs s (vs, h) v' -> forall vs', agree_in vs vs' (ArgVars f) -> exists vs'', RunsTo fs s (vs', h) (vs'', snd v') /\ sel vs'' (RetVar f) = sel (fst v') (RetVar f).
      intros.
      eapply NoUninitialized_RunsTo in H0; eauto.
      destruct H; intuition.
    Qed.

  End TopSection.

End Make.

author: mit-plv

repo: bedrock

save_path: github-repos/coq/mit-plv-bedrock


text:
Require Export Core.Basics.

(* Replaces a default element with a proof that n is in-bounds. *)
Fixpoint safe_nth [A] (n : nat) (l : list A) : n < length l -> A :=
  match n, l with
  (* impossible cases *)
  | 0,   []      => λ p : 0 < length [], match Lt.lt_irrefl _ p with end
  | S k, []      => λ p : S k < length [], match Lt.lt_n_0 _ p with end
  (* possible cases *)
  | 0,   x :: _  => λ _, x
  | S k, x :: xs => λ p : S k < length (x :: xs), safe_nth k xs (Lt.lt_S_n _ _ p)
  end.

Lemma Forall_singleton : ∀ (A : Type) (P : A -> Prop) x, List.Forall P [x] <-> P x.
Proof.
  split; intros.
  - exact (Forall_inv H).
  - exact (Forall_cons x H (Forall_nil _)).
Qed.

Lemma Exists_singleton : ∀ (A : Type) (P : A -> Prop) x, List.Exists P [x] <-> P x.
Proof.
  split; intros.
  - apply Exists_cons in H; destruct H; [ auto | apply Exists_nil in H; contradiction ].
  - apply Exists_cons_hd. exact H.
Qed.

Lemma Forall_map (A B : Type) (P : B -> Prop) (f : A -> B) (xs : list A) : List.Forall P (List.map f xs) <-> List.Forall (P ∘ f) xs.
Proof with cbn.
  induction xs...
  - firstorder.
  - change (a :: xs) with ([a] ++ xs).
    rewrite Forall_app, Forall_singleton.
    change (f a :: List.map f xs) with ([f a] ++ List.map f xs).
    rewrite Forall_app, Forall_singleton.
    split.
    * intros; destruct H.
      split; try assumption.
      rewrite <- IHxs.
      exact H0.
    * intros; destruct H.
      split; try assumption.
      rewrite -> IHxs.
      exact H0.
Qed.

Lemma Exists_map (A B : Type) (P : B -> Prop) (f : A -> B) (xs : list A) : List.Exists P (List.map f xs) <-> List.Exists (P ∘ f) xs.
Proof with cbn.
  induction xs...
  - split; intros; apply Exists_nil in H; contradiction.
  - change (a :: xs) with ([a] ++ xs).
    rewrite Exists_app, Exists_singleton.
    change (f a :: List.map f xs) with ([f a] ++ List.map f xs).
    rewrite Exists_app, Exists_singleton.
    split.
    * intros; destruct H.
      + left. exact H.
      + right. apply IHxs. exact H.
    * intros; destruct H.
      + left. exact H.
      + right. apply IHxs. exact H.
Qed.

Lemma forall_imp_Forall {A : Type} (f g : A -> Prop) (xs : list A) : (∀ x, f x -> g x) -> List.Forall f xs -> List.Forall g xs.
Proof.
  intros p H.
  induction xs.
  - apply Forall_nil.
  - apply Forall_cons.
    * apply Forall_inv in H.
      exact (p a H).
    * apply Forall_inv_tail in H.
      exact (IHxs H).
Qed.

author: ConorReynolds

repo: coq-institutions


text:
Set Implicit Arguments.

Require Import Bedrock.Platform.AutoSep.
Require Import Bedrock.Platform.Facade.examples.FiatADTs.
Import Adt.
Require Import Bedrock.Platform.Cito.RepInv.

Require Import Bedrock.Platform.Facade.examples.FiniteSetF Bedrock.Platform.Facade.examples.ListSetF Bedrock.Platform.Facade.examples.SeqF Bedrock.Platform.Facade.examples.ListSeqF.

Definition rep_inv p adtvalue : HProp :=
  match adtvalue with
    | List ls => lseq ls p
    | Junk _ => [| False |]
    | FEnsemble s => lset s p
  end%Sep.

Module Ri <: RepInv FiatADTs.Adt.

  Definition RepInv := W -> ADTValue -> HProp.

  Definition rep_inv := rep_inv.

  Lemma rep_inv_ptr : forall p a, rep_inv p a ===> p =?> 1 * any.
    destruct a; simpl.
    eapply Himp_trans; [ apply lseq_fwd | sepLemma ]; apply any_easy.
    sepLemma.
    eapply Himp_trans; [ apply lset_fwd | sepLemma ]; apply any_easy.
  Qed.

End Ri.


text:
(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2.1 FREE SOFTWARE LICENSE AGREEMENT        *)
(**************************************************************)

Require Import Arith Lia Euclid Utf8.

(* P is computationally decidable *)
Definition dec P := { P } + { ¬ P }.

Fact conj_dec (A B : Prop) : dec A → dec B → dec (A∧B).
Proof. unfold dec; tauto. Qed.

Section minimizer.

  (* Minimization of a decidable and inhabited subset of nat, following
     Constructive Epsilon from the standard library
   *)

  Variable (P : nat → Prop) (Pdec : ∀n, dec (P n)).

  Let Ω n m := n = S m ∧ ¬ P m.

  Section exP_Acc.

    Let HR1 n : P n → Acc Ω n.
    Proof. constructor; now intros ? (? & []). Qed.

    Let HR2 n : Acc Ω (S n) → Acc Ω n.
    Proof. constructor; now intros ? (-> & _). Qed.

    Local Fact exP_Acc0 : (∃n, P n) → Acc Ω 0.
    Proof.
      intros (n & Hn%HR1); revert Hn.
      generalize 0 n (Nat.le_0_l n).
      induction 1; auto.
    Qed.

  End exP_Acc.

  (* NB n := P holds Not Before n
     MIN := first value such that P *)
  Let NB m := ∀i, P i → i < m → False.
  Let MIN := { m | P m ∧ NB m }.

  Let NB_0 : NB 0.
  Proof. now intros _ _ ?%Nat.nlt_0_r. Qed.

  Let NB_S n : NB n → ¬ P n → NB (S n).
  Proof.
    intros H1 H2 i H3 H4%le_S_n.
    destruct H4.
    + apply H2, H3.
    + apply (H1 _ H3), le_n_S, H4.
  Qed.

  Let Fixpoint loop n (an : Acc Ω n) { struct an } : NB n → MIN.
    refine (match Pdec n with
    | left pn  => λ hn, exist _ n _
    | right pn => λ hn, loop (S n) (Acc_inv an _) _
    end); [ | red | ]; auto.
  Qed.

  (** Notice that this "mnimizer" principle cannot be proved by
      induction on n only unless one assumes { n | P n } instead
      of the (generally) weaker (∃n, P n). These two are here
      equivalent because P is decidable over an enumerable type.

      The weaker form { n | P n } → MIN (or equivalently
      ∀n, P n → MIN) can be proved by induction on n and
      this would be enough as a minimization principle
      for the proof of √2 below. *)

  Definition minimizer : (∃n, P n) → MIN :=
    λ hn, loop 0 (exP_Acc0 hn) NB_0.

End minimizer.

Definition divides p q := ∃k, k*p = q.

Notation "p 'div' q" := (divides p q) (at level 70).

Fact remainder_is_zero p a b r : r < p → a*p = b*p+r → r = 0.
Proof.
  intros H1 H2.
  assert ((a-b)*p = r) as C.
  + rewrite Nat.mul_sub_distr_r; lia.
  + destruct (a-b); lia.
Qed.

Fact divides_dec p q : dec (p div q).
Proof.
  destruct p as [ | p ].
  + destruct q as [ | q ].
    * left; exists 0; auto.
    * right; intros (k & Hk); now rewrite Nat.mul_comm in Hk.
  + destruct (eucl_dev (S p)) with (m := q)
      as [ x [ | r ] Hr E ]; try lia.
    * left; exists x; lia.
    * right; intros (k & <-).
      apply remainder_is_zero in E; lia.
Qed.

(* Computes the quotient from assumption of divisibility *)
Fact quotient p q : 0 < p → p div q → { x | x*p = q }.
Proof.
  intros H1 H2.
  destruct (eucl_dev _ H1 q) as [ x r H3 H4 ].
  exists x.
  destruct H2 as (k & <-).
  generalize (remainder_is_zero _ _ _ _ H3 H4); lia.
Qed.

Section sqrt2.

  (** We assume a fraction p/q "equal" to √2, ie of which the square is 2 *)
  Variables (p q : nat) (Hq : 0 < q) (Hpq : p*p = 2*q*q).

  (** Below, we manipulate √2 in nat as p/q *)

  Let Hp : 0 < p.
  Proof. destruct p; lia. Qed.

  (* REMARKS & QUESTIONS:
       1) we can replace the minimizer
            ∀P, dec P → (∃n, P n) → { m | P m ∧ ∀i, P i → i < m → False }
          with the weaker form
            ∀P, dec P → ∀n, P n → { m | P m ∧ ∀i, P i → i < m → False }
          and the below proof would still work.
       2) the weaker minimizer can be proved by (strong) induction on n
       3) can we replace the use of the minimizer directly with strong
          induction on the proof below ? *)

  (** Let us build k minimal such that k√2 is strictly positive integer *)

  Let Q k := 0 < k ∧ q div k*p.

  Let k_full : { k | Q k ∧ ∀i, Q i → i < k → False }.
  Proof.
    apply minimizer.
    + intro; apply conj_dec; [ apply lt_dec | apply divides_dec ].
    + exists q; split; auto.
      exists p; ring.
  Qed.

  Let k := proj1_sig k_full.

  Let Hk0 : 0 < k.
  Proof. apply (proj2_sig k_full). Qed.

  (* k√2 is integer *)
  Let Hk1 : q div k*p.
  Proof. apply (proj2_sig k_full). Qed.

  (* k is minimal for 0 < k and k√2 integer *)
  Let Hk2 : ∀i, Q i → i < k → False.
  Proof. apply (proj2_sig k_full). Qed.

  (** Let us build d = k√2 = kp/q *)

  Let d_full : { d | d*q = k*p }.
  Proof. now apply quotient. Qed.

  Let d := proj1_sig d_full.

  (* d = k√2 *)
  Let Hd0 : d*q = k*p.
  Proof. apply (proj2_sig d_full). Qed.

  (* d² = 2k² *)
  Let Hd1 : d*d = 2*k*k.
  Proof.
    rewrite <- Nat.mul_cancel_r with (p := q); try lia.
    rewrite <- (Nat.mul_assoc d), Hd0, Nat.mul_comm.
    rewrite <- Nat.mul_cancel_r with (p := q); try lia.
    rewrite <- (Nat.mul_assoc _ d), Hd0.
    rewrite (Nat.mul_comm k) at 2.
    rewrite Nat.mul_assoc, <- (Nat.mul_assoc k p), Hpq.
    ring.
  Qed.

  (* d is strictly larger than k *)
  Let Hd2 : k < d.
  Proof.
    destruct (le_lt_dec d k); auto.
    assert (2*k*k <= k*k) as C; try lia.
    rewrite <- Hd1.
    now apply Nat.mul_le_mono.
  Qed.

  (** Now we consider k' := k√2-k = k(√2-1) *)

  Let k' := d-k.

  (* k' is strictly below k *)
  Let Hk1' : k' < k.
  Proof.
    destruct (le_lt_dec k k') as [ C | ]; auto.
    apply Nat.mul_le_mono_l with (p := k) in C.
    unfold k' in C; rewrite !Nat.mul_sub_distr_l in C.
    lia.
  Qed.

  (* k' satisfies Q *)
  Let Hk2' : Q k'.
  Proof.
    split; unfold k'.
    + lia.
    + exists (2*k-d).
      unfold k'.
      rewrite !Nat.mul_sub_distr_r.
      f_equal; auto.
      rewrite <- Nat.mul_cancel_r with (p := d); try lia.
      rewrite <- !Nat.mul_assoc, (Nat.mul_comm q), Hd0, !Nat.mul_assoc, <- Hd1.
      ring.
  Qed.

  (* By minimality of k, we get a contradiction *)
  Theorem sqrt2_nat_false : False.
  Proof. exact (Hk2 _ Hk2' Hk1'). Qed.

  (** Concluding remarks: the above proof works as
      well (and nearly as is) for √3 but fails for eg √5.
      This is because while we have 1 < √2 (or √3) < 2,
      √5 > 2 does not enjoy this property.

      Can we upgrade so proof to deal with √u where u is
      not a square integer? For instance, can we use this
      proof to show √u = p/q (ie p² = uq²) to imply that
      there is r st u = r² ?

      Can this even be upgraded to an algorithm for
      computing the square root ? *)

End sqrt2.

Check sqrt2_nat_false.

author: DmxLarchey


(** * Bicolano: Big step (interface implementation) *)

(* <Insert License Here>

    $Id: BigStep.v 68 2006-02-02 15:06:27Z davidpichardie $ *)

(** Big step semantics.

 @author David Pichardie *)

(* Hendra : - Modified to suit DEX program.
            - Also trim the system to contain only Arithmetic *)

Require Export DEX_BigStepType.
Require Export DEX_ImplemDomain.

Open Scope type_scope.

Module DEX_BigStep <: DEX_BIGSTEP.

  Module DEX_Dom := DEX_ImplemDomain.DEX_Dom.

  (* Inductive definition are put in BigStepLoad.v.
     They are shared with BigStepType.v *)
  Load "DEX_BigStepLoad.v".

  Lemma IntraStep_ind_ :
      forall (p:DEX_Program) (P:DEX_Method->DEX_IntraNormalState->DEX_IntraNormalState+DEX_ReturnState->Prop),
         (forall m s, P m s (inl _ s)) ->
         (forall m s r, DEX_exec_return p m s r -> P m s (inr _ r)) ->
         (forall m s s' , DEX_exec_intra p m s s' ->
            forall r, DEX_IntraStepStar p m s' r -> P m s' r ->
            P m s r) ->
      forall m s r, DEX_IntraStep p m s r ->
        match r with
        | inr r' => P m s (inr _ r')
        | inl s' => forall r', DEX_IntraStepStar p m s' r' -> P m s' r' -> P m s r'
        end.
     Proof.
       intros p P H0 Hr Hi Hcr Hc.
       fix intra 2;intros r Hs;case Hs;clear r Hs;intros.
       apply Hr;trivial.
       apply Hi with s2;trivial.
     Qed.

  Lemma IntraStepStar_ind :
    forall (p:DEX_Program)
     (P : DEX_Method -> DEX_IntraNormalState -> DEX_IntraNormalState + DEX_ReturnState -> Prop),
       (forall m s, P m s (inl _ s)) ->
       (forall m s r, DEX_exec_return p m s r -> P m s (inr _ r)) ->
       (forall m s s' , DEX_exec_intra p m s s' ->
          forall r, DEX_IntraStepStar p m s' r -> P m s' r ->
          P m s r) ->
    forall m s r, DEX_IntraStepStar p m s r -> P m s r.
   Proof.
     intros p P H0 Hr Hi.
     fix fixp 4; intros m s' s Ht;case Ht;clear Ht s' s;intros.
     apply H0.
     generalize (IntraStep_ind_ p P H0 Hr Hi _ _ _ H).
     case r;intros;trivial.
     apply H1;trivial. constructor.
     assert (HH:=IntraStep_ind_  p P H0 Hr Hi _ _ _ H);simpl in HH.
     apply HH;trivial.
     apply fixp;trivial.
   Qed.

  Lemma IntraStepStar_intra_ind :
    forall (p:DEX_Program)
     (P : DEX_Method -> DEX_IntraNormalState -> DEX_IntraNormalState -> Prop),
       (forall m s, P m s s) ->
       (forall m s s', DEX_exec_intra p m s s' ->
          forall s'', DEX_IntraStepStar_intra p m s' s'' -> P m s' s'' ->
          P m s s'') ->
    forall m s s', DEX_IntraStepStar_intra p m s s' -> P m s s'.
   Proof.
     intros p P H0 Hi Hc.
     assert (forall m s r, DEX_IntraStepStar p m s r ->
              forall s', r = inl _ s' -> P m s s').
      induction 1 using IntraStepStar_ind;intros;try discriminate;subst;eauto.
      inversion H;auto.
     intros; eapply H; eauto.
   Qed.

  Lemma BigStep_ind :
    forall (p:DEX_Program)
     (P : DEX_Method -> DEX_IntraNormalState -> DEX_ReturnState -> Prop),
       (forall m s r, DEX_exec_return p m s r -> P m s r) ->
       (forall m s s' , DEX_exec_intra p m s s' ->
          forall r, DEX_BigStep p m s' r -> P m s' r ->
          P m s r) ->
    forall m s r, DEX_BigStep p m s r -> P m s r.
  Proof.
   intros p P Hr Hi Hcr Hc.
   assert (forall m s R, DEX_IntraStepStar p m s R -> forall r, R = inr _ r -> P m s r).
   induction 1 using IntraStepStar_ind;intros r0 Heq;try inversion Heq;subst;
    try (eauto;fail).
   intros;eapply H;eauto.
  Qed.

  Lemma ReachableStar_ind :
    forall (p:DEX_Program)
     (P : (DEX_Method * DEX_IntraNormalState) -> (DEX_Method * DEX_IntraNormalState) -> Prop),
       (forall m s, P (m,s) (m,s)) ->
       (forall m s s', DEX_exec_intra p m s s' ->
          forall m' s'', ClosReflTrans (DEX_ReachableStep p) (m,s') (m',s'') ->
          P (m,s') (m',s'') ->
          P (m,s) (m',s'')) ->
    forall ms ms',
       ClosReflTrans (DEX_ReachableStep p) ms ms' -> P ms ms'.
   Proof.
     intros p P H0 Hi Hc Hsc.
     induction 1;intros.
     destruct a;eauto.
     destruct a'' as (m'',s'').
     inversion H;subst;eauto.
     inversion H2;clear H2;subst;eauto.
   Qed.

End DEX_BigStep.


text:
Require Export plik.

Definition tutu (X : Set) := toto X.

repo: Coq-misc


text:
Require Import Common.

Inductive type : Type :=
| Tlift : type0 -> type
| Tsum : list type -> type
| Ttuple : list type -> type.

Fixpoint eval_type (t : type) :=
  match t with
    | Tlift t => eval_type0 t
    | Tsum l =>
        List.fold_right (fun x acc => eval_type x + acc)%type Datatypes.unit l
    | Ttuple l =>
        List.fold_right (fun x acc => eval_type x * acc)%type Datatypes.unit l
  end.

Inductive sync : Type :=
  | Treg : forall (t : type), sync.

Definition state := list sync.
Definition eval_sync (s : sync) := match s with Treg t => eval_type t end.
Definition eval_state := eval_env eval_sync.

Notation Int := (Tlift (Tint 16)).
Notation Bool := (Tlift (Tbool)).
Notation Unit := (Tlift (Tunit)).

Inductive member {T} : list T -> Type :=
| member_0 : forall l t, member (t::l)
| member_S : forall l t, member l -> member (t :: l).

Record sync_signature Phi T (E : T -> Type) :=
  {
    sy_args : list T;
    sy_res : T;
    sy_value : Phi -> eval_env E sy_args -> E sy_res * Phi
  }.

Record module (T : Type) :=
  {
    methods : list (sync_signature T type eval_type);
    accs : member methods
  }.

Arguments methods {T} m.
Section t.
  Variable A B : Type.
  Variable ma : module A.
  Variable mb : module B.

  Definition mab : module (A * B)%type :=
    {|
      methods := List.app (methods ma) (methods mb)
    |}.

  apply
Section s.

  Variable Phi : state.
  Variable primitive : element Phi -> list type -> type -> Type.

  Section t.

    Variable Var : type -> Type.
    Inductive expr :  type -> Type :=
    | Evar : forall t (v : Var t), expr t
    | Ebuiltin : forall args res (f : builtin args res),
                   dlist  (fun j => expr (Tlift j)) (args) ->
                   expr  (Tlift res)
    | Econstant : forall  (c : constant), expr (Tlift (cst_ty c))
    | Etuple : forall l (exprs : dlist (expr) l), expr (Ttuple l)
    | Econstructor :  forall l t (cn: var l t) (arg : expr t),  expr (Tsum l)
    | Ematch : forall l t'
                 (arg : expr (Tsum l))
                 (cases : dlist (fun t => Var t -> expr t') (l))
                 (default : expr t'),
                 expr t'.

    Inductive action : type -> Type :=
    | Return : forall t (exp : expr t), action t
    | Bind :
      forall t u
        (a : action  t)
        (f : Var t -> action u),
        action u
    | When : forall t (e : expr Bool) (a : action t), action t
    | Primitive :
      forall A args res (p : primitive A args res)
        (exprs : dlist (expr) args),
        action res
    | Case :
      forall l t t'
        (which : var l t)
        (arg : expr (Tsum l))
        (f :Var t -> action t'),
        action t'.

  End t.

  Notation eval_type_list := (List.fold_right (fun x acc => eval_type x * acc)%type Datatypes.unit).

  Definition eval_expr (t : type) (e : expr eval_type t) : eval_type t.
  refine (
      let fix eval_expr t e {struct e}:=
          match e with
            | Evar t v => v
            | Ebuiltin args res f x =>
                let exprs :=
                    _
                in
                builtin_denotation args res f exprs
            | Econstant c => cst_val c
            | Etuple l exprs =>
                dlist_fold'  _ _ _ eval_expr l exprs
            | Econstructor l t cn arg =>
                _
            | Ematch l t' arg cases default =>
                _
          end
      in eval_expr t e).

  refine (let fix fold l (dl : dlist (fun j => expr eval_type (Tlift j)) l) : eval_env eval_type0 l :=
      match dl with
          | dlist_nil => tt
          | dlist_cons _ _ t q => (eval_expr _ t,fold _ q)
      end in fold args x).

  refine (let fix fold l t (v : var l t):  eval_type t -> eval_type (Tsum  l) :=
              match v in var l t return eval_type t -> eval_type (Tsum l) with
                | var_0 l b => fun x => inl x
                | var_S l _ _ v'  => fun x => inr (fold _ _ v' x)
              end in fold l t1 cn (eval_expr _ arg)).

  refine (let fix fold l (cases : dlist (fun t => eval_type t -> expr eval_type t') l) :
              eval_type (Tsum l) ->
              eval_type t' :=
              match cases with
                | dlist_nil => fun  _ => eval_expr _ default
                | dlist_cons a b t q => fun (arg : eval_type (Tsum (a::b))) =>
                           match arg with
                               | inl x => eval_expr _ (t x)
                               | inr x =>  fold _ q x
                           end
              end
          in fold l cases (eval_expr _ arg)
         ).

  Defined.

  (** dynamic semantics:
    - all guard failures are represented by None.
    - continuation passing style: the current diff is threaded through the execution
  *)

  Variable diff : Type.
  Definition T t := eval_state Phi -> diff -> option (t * diff).
  Definition ret {t} (e : t) : T t  := fun st d => Some (e, d).
  Definition bind {s t} : T s -> (s -> T t) -> T t :=
    fun (x : T s) (f : s -> T t) (st : eval_state Phi) (d : diff) =>
      match x st d with
          Some (e, d') =>  f e st d'
        | None => None
      end.
  Definition fail {t} : T t := fun _ _ => None.

  Definition eval_action (t : type) (a : action eval_type t) :
    (T (eval_type t)).
  refine (
      let fix eval_action (t : type) (a : action eval_type t) :
          T ( eval_type t) :=
          match a with
            | Return t exp => ret (eval_expr _ exp)
            | Bind t u a f =>
                let act := eval_action _ a in
                let f' := (fun e => eval_action u (f e)) in
                  bind act f'
            | When t e a =>
                let g1 := eval_expr _ e in
                let a' := eval_action t a in
                match g1 with
                  | true => a'
                  | false => fail
                end
            | Primitive A args res p exprs => _
            | Case l t t' which arg f =>
                _
          end
      in  eval_action t a).
  clear. admit.
  refine (let fix fold t l (v : var l t) : eval_type (Tsum l) -> option (eval_type t) :=
          match v with
            | var_0 a b => fun X => match X with inl X => Some X | _ => None end
            | var_S E t1 t2 v' =>
                     fun X : eval_type (Tsum (t1 :: E)) =>
                       match X with
                         | inl _ => None
                         | inr X0 => fold t2 E v' X0
                       end
          end
          in
            match fold _ _ which (eval_expr _ arg) with
              | None => fail
              | Some r => eval_action _ (f r)             end
         ).
  Defined.
  Definition Action t := forall Var, action Var t.
  Definition Expr t := forall Var, expr Var t.
End s.

(* Definition Const (n : Z) : Expr (Int) := *)
(*   fun _ =>  Econstant _ (Build_constant (Tint 16) (Word.repr 16 n)). *)

(* Definition Plus (E1 E2 : Expr Int) : Expr Int := *)
(*   fun _ => Ebuiltin _ (W 16 :: W 16 :: nil) _  (BI_plus 16) (dlist_cons E1 (dlist_cons E2 dlist_nil)).  *)
(* Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := *)
(*   fun _ => App' (F _) (X _). *)
(* Definition  *)
(* Section st.  *)
(*   Variable A B : Type.  *)
(*   Variable PA : A -> list type -> type -> Type.  *)
(*   Variable PB : B -> list type -> type -> Type.  *)
(*   Definition C := (A * B)%type.  *)

(* Arguments Bind {Phi primitive Var t u} _ _.  *)
(* Arguments Primitive {Phi primitive Var} A {args res} p _ .  *)

(* Definition register (ty : type) : effects. Admitted.  *)

(* Inductive register_ops (ty : type) : register ty -> list type -> type -> Type := *)
(*   | Write : forall E, register_ops ty E (cons ty nil) unit *)
(*   | Read  : forall E, register_ops ty E nil ty.  *)

(* Definition Num : type := Tlift (Tint 32).  *)
(* Require Import List.  *)
(* Definition Val : type := Tsum ((Ttuple (Num :: Num :: nil) :: (Ttuple (Num :: nil)) :: nil )).  *)

(* Let R := register Val.  *)
(* Definition iterate : Action R (register_ops Val) unit.  *)
(* intros Var.  *)
(* Notation "'DO' X <- A ; B" := (Bind A (fun X => B)) *)
(*   (at level 200, X ident, A at level 100, B at level 200).  *)

(* Section st.  *)

(* refine (DO X <- _ ; _).  *)
(* eapply Primitive.  *)
(* eapply Read. apply dlist_nil.  *)
(* refine (DO Y <- Case _ _ _ _ _ _ var_0 (Evar _ _  X) _ ; _).  *)

(* Focus 2.  *)

(* 2: refine (Primitive _ (register_ops Val) _ (Read R )).  *)
(* Definition mod_iterate_rule : rule [Treg Val].  *)
(* set (env := [Treg Num; Treg Num]).  *)
(* set (a := var_0 : var env (Treg Num)).  *)
(* set (b := var_S var_0 : var env (Treg Num)).  *)
(* apply (mk_rule' env).  *)

(* Definition pattern2_vector_singleton E t x := *)
(*   pattern2_vector_cons E _ t _ x pattern2_vector_nil.  *)
(* apply (pattern2_vector_singleton env).  *)
(* apply Plift.  *)
(* eapply Punion.  apply  (pattern1_disjunct_hd).  *)
(* apply ([| Pvar1 Num, Pvar1 Num |])%pattern.  *)

(* apply (! b <= ! a)%expr.  *)

(* Definition expr2_vector_singleton E t (x : @expr2 E t) : expr2_vector E [t] := *)
(*   dlist_cons x (@dlist_nil type2 (expr2 E)).  *)

(* apply expr2_vector_singleton.  *)
(* eapply Eset. eapply Eunion. eapply expr1_disjunct_hd.  apply ([| !a - !b, !b|])%expr.  *)
(* Defined.  *)

(* Definition mod_done_rule : rule [Treg Val].  *)
(* set (env := [Treg Num; Treg Num]).  *)
(* set (a := var_0 : var env (Treg Num)).  *)
(* set (b := var_S var_0 : var env (Treg Num)).  *)
(* apply (mk_rule' env).  *)

(* apply (pattern2_vector_singleton env).  *)
(* apply Plift. eapply Punion. apply pattern1_disjunct_hd.  *)
(* apply ([| Pvar1 Num, Pvar1 Num |])%pattern.  *)

(* apply (!a < !b)%expr.  *)

(* apply expr2_vector_singleton.  *)
(* apply Eset.  *)
(* apply Eunion. apply expr1_disjunct_tl. apply expr1_disjunct_hd. *)
(* apply ([| !a |])%expr.  *)
(* Defined.  *)

(* Definition TRS : TRS := *)
(*   {| trs_type := [Treg Val];  *)
(*      trs_rules := [mod_iterate_rule; mod_done_rule ]|}.  *)

(* Definition AA : Word.T 32 := Word.repr 32 31.  *)
(* Definition BB : Word.T 32 := Word.repr 32 3.  *)

(* Definition this_ENV : eval_env eval_type2 [Treg Num; Treg Num] := (AA, (BB, tt)).  *)

(* Eval compute in run_unfair 10 TRS ((inl this_ENV, tt)).  *)

author: braibant

repo: Synthesis

save_path: github-repos/coq/braibant-Synthesis


text:
Require Export List.
Require Export Bool.
Require Export Arith.
Require Export Peano_dec.
Require Export Coq.Arith.PeanoNat.
Require Export Coq.Program.Wf.
Require Export Coq.Program.Tactics.
Require Export Coq.Logic.FunctionalExtensionality.
Require Export Recdef.

Require Import common.CpdtTactics.
Require Import common.wyv_common.
Require Import common.rhs_mat_tree.

Import WfExtensionality.

Lemma subtype_equ_equ_reduce :
  forall T1 L1 T1', T1 = (t_equ L1 T1') ->
               forall T2 L2 T2', T2 = (t_equ L2 T2') ->
                            subtype T1 T2 = andb (eq_label L1 L2)
                                                 (andb (subtype T1' T2')
                                                       (subtype T2' T1')).
Proof.
  intros.

  remember (subtype T1 T2) as sub_fn; subst T1 T2.

  unfold subtype, subtype_func in Heqsub_fn;
    simpl in Heqsub_fn;
    rewrite fix_sub_eq_ext in Heqsub_fn;
    simpl in Heqsub_fn;
    fold subtype_func in Heqsub_fn;
    auto.
Qed.

author: JulianMackay


text:
From DeepWeb Require Import
     Common
     Switch.
Import
  SumNotations.
Open Scope list_scope.
Global Open Scope sum_scope.

CoFixpoint compose' {E T} `{Is__nE E}
           (bfi bfo : list packetT)
           (net     : itree nE T)
           (app     : itree netE T) : itree E T :=
  match observe net, observe app with
  | RetF r, _
  | _, RetF r => Ret r
  | TauF net', _ => Tau (compose' bfi bfo net' app)
  | _, TauF app' => Tau (compose' bfi bfo net  app')
  | VisF vn kn, VisF va ka =>
    let step__net :=
        match vn with
        | (e|) =>
          match e in nondetE Y return (Y -> _) -> _ with
          | Or =>
            fun k =>
              b <- trigger Or;;
              Tau (compose' bfi bfo (k b) app)
          end kn
        | (|e|) =>
          match e in logE Y return (Y -> _) -> _ with
          | Log str =>
            fun k =>
              embed Log ("Switch: " ++ str)%string;;
              Tau (compose' bfi bfo (k tt) app)
          end kn
        | (||e) =>
          match e in netE Y return (Y -> _) -> _ with
          | Net__Select =>
            fun k =>
              conns <- trigger Net__Select;;
              Tau (compose' bfi bfo (k (map packet__src bfo ++ conns)) app)
          | Net__Recv c =>
            fun k =>
              if conn_is_app c
              then
                match pick (Nat.eqb c ∘ packet__src) bfo with
                | Some (pkt, bo') =>
                  Tau (compose' bfi bo' (k pkt) app)
                | None            => ITree.spin (* should not happen *)
                end
              else
                pkt <- embed Net__Recv c;;
                Tau (compose' bfi bfo (k pkt) app)
          | Net__Send pkt =>
            fun k =>
              if conn_is_app (packet__dst pkt)
              then Tau (compose' (bfi ++ [pkt]) bfo (k tt) app)
              else
                embed Net__Send pkt;;
                Tau (compose' bfi bfo (k tt) app)
          end kn
        end in
    let step__app :=
        match va in netE Y return (Y -> _) -> _ with
        | Net__Select =>
          fun k =>
            let cs : list connT := map packet__src bfi in
            match cs with
            | [] =>
              (* embed Log ("App selected nothing, step net");; *)
              step__net
            | _ :: _ => Tau (compose' bfi bfo net (k cs))
            end
        | Net__Recv c =>
          fun k =>
            match pick (Nat.eqb c ∘ packet__src) bfi with
            | Some (pkt, bi') =>
              Tau (compose' bi' bfo net (k pkt))
            | None =>
              (* embed Log ("App received nothing, step net");; *)
              step__net
            end
        | Net__Send pkt =>
          fun k => Tau (compose' bfi (bfo ++ [pkt]) net (k tt))
        end ka in
    step__app
  end.

Definition compose_switch {E T} `{Is__nE E}
  : itree nE T -> itree netE T -> itree E T :=
  compose' [] [].

author: liyishuai

repo: DeepWebTest

save_path: github-repos/coq/liyishuai-DeepWebTest


text:
(** Atividade sobre os numerais de Church. Adaptado de [Pierce:SF]. *)

Definition admit {T: Type} : T.  Admitted.

(** Tipo dos numerais. *)
Definition num := forall X : Type, (X -> X) -> X -> X.

(** Alguns numerais. *)
Definition zero : num :=
  fun (X : Type) (f : X -> X) (x : X) => x.

Definition um : num :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

Definition dois : num :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).

Definition tres : num :=
  fun (X : Type) (f : X -> X) (x : X) => f (f (f x)).

(** Exercício 1: Defina a função sucessor. *)
Definition suc (n : num) : num :=
  fun (X: Type) (f : X -> X) (x : X) => f (n X f x).

(** Exercício 2: Prove os seguintes fatos: *)
Example suc_1 : suc zero = um.
Proof.
  apply suc.
  - unfold num.
    intros.
    assumption.
  - intro H.
    unfold suc.
    unfold zero.
    unfold um.
    reflexivity.
  - unfold suc.
    unfold zero.
    unfold um.
    reflexivity.
Qed.

Example suc_2 : suc um = dois.
Proof.
  unfold suc.
  unfold um.
  unfold dois.
  reflexivity.
Qed.

Example suc_3 : suc dois = tres.
Proof.
  unfold suc.
  unfold dois.
  unfold tres.
  reflexivity.
Qed.

(**
De uma forma geral podemos gerar o numeral de Church Cn, dado o natural n.
 *)

Fixpoint ch (n:nat) : num :=
  match n with
    | O => zero
    | S k => suc (ch k)
  end.

Compute (ch 0).
Compute (ch 1).
Compute (ch 2).
Compute (ch 3).

(** Exercício 3: *)
Theorem suc_S: forall n,  suc (ch n) = (ch (S n)).
Proof.
  intro n.
  simpl ch.
  reflexivity.
Qed.

(** Exercício 4: Defina a adição de dois numerais. *)
Definition soma (n m : num) : num :=
  fun (X : Type) (f: X->X) (x: X) => m X f (n X f x).

(** Exercício 5: Prove os seguintes fatos: *)
Example soma_1 : soma zero um = um.
Proof.
  unfold soma.
  unfold zero.
  unfold um.
  reflexivity.
Qed.

Example soma_2 : soma dois tres = soma tres dois.
Proof.
  unfold soma.
  unfold dois.
  unfold tres.
  reflexivity.
Qed.

Example soma_3 :
  soma (soma dois dois) tres = soma um (soma tres tres).
Proof.
  unfold soma.
  unfold dois.
  unfold tres.
  unfold um.
  reflexivity.
Qed.

(** Exercício 6: *)
Theorem suc_soma: forall n m, suc(soma n m) = soma (suc n) m.
Proof.
  intros n m.
  unfold suc.
  unfold soma.
  (* reflexivity. *)
Admitted.

(** Exercício 7: *)
Theorem suc_soma': forall n m, suc(soma (ch n) m) = soma (ch n) (suc m).
  intros n m .
  unfold ch.
  unfold suc.
  unfold soma.
  unfold zero.
  reflexivity.
Qed.

(** Exercício 8: *)
Theorem suc_soma_zero: forall m, suc(soma zero m) = soma zero (suc m).
Proof.
  intro m.
  unfold soma.
  unfold suc.
  reflexivity.
Qed.

(** Exercício 9: *)
Theorem soma_com: forall n m, soma  (ch n) (ch m) = soma (ch m) (ch n).
Proof.
  induction n.
  - intro m.
    simpl ch.
    unfold soma.
    unfold zero.
    reflexivity.
  - intro m.
    simpl ch.
    rewrite <- suc_soma.
    rewrite -> IHn.
    unfold suc.
    unfold soma.
    reflexivity.
Qed.

(** Exercício 10: *)
Theorem soma_zero_dir: forall n, soma (ch n) zero = (ch n).
Proof.
  intro n.
  unfold soma.
  unfold zero.
  reflexivity.
Qed.

(** Exercício 11: *)
Theorem soma_zero_esq: forall n, soma zero n = n.
Proof.
  intro n.
  unfold soma.
  unfold zero.
  reflexivity.
Qed.

(** Exercício 12: *)
Theorem suc_soma_um: forall n, suc (ch n) = soma um (ch n).
Proof.
  intro n.
  induction n.
  - unfold suc.
    unfold soma.
    unfold um.
    reflexivity.
  - simpl ch.
    rewrite -> IHn.
    rewrite -> suc_soma.
    unfold um.
    unfold soma.
    unfold suc.
    reflexivity.
Qed.

(** Exercício 13: *)
Theorem soma_assoc: forall n m k, soma (soma n m) k = soma n (soma m k).
Proof.
  intros n m k.
  unfold soma.
  reflexivity.
Qed.

(** Exercício 14: Defina a multiplicação de dois numerais. *)
Definition mult (n m : num) : num :=
  fun (X : Type) (f: X -> X) => m X (n X f).

(** Exercício 15: Prove os seguintes fatos: *)
Example mult_1 : mult um um = um.
Proof.
  unfold mult.
  unfold um.
  reflexivity.
Qed.

Example mult_2 : mult zero (soma tres tres) = zero.
Proof.
  unfold mult.
  unfold zero.
  unfold soma.
  unfold tres.
  reflexivity.
Qed.

Example mult_3 : mult dois tres = soma tres tres.
Proof.
  unfold mult.
  unfold dois.
  unfold tres.
  unfold soma.
  reflexivity.
Qed.

(** Exercício 16: *)
Theorem mult_zero_dir: forall n, mult (ch n) zero = zero.
Proof.
  intro n.
  unfold mult.
  unfold zero.
  reflexivity.
Qed.

(** Exercício 17: *)
Theorem mult_zero_esq: forall n, mult zero (ch n) = zero.
Proof.
  intro n.
  induction n.
  - unfold zero.
    unfold mult.
    reflexivity.
  - rewrite <- IHn.
    unfold zero.
    unfold mult.
    simpl ch.
    unfold suc.
   (*  reflexivity. *)
Admitted.

(** Exercício 18: Defina a exponenciação de dois numerais. *)
Definition exp (n m : num) : num :=
  fun (X: Type) (f: X -> X) (x: X) => m (n f x).

(** Exercício 19: Prove os seguintes fatos: *)
Example exp_0 : exp um um = um.
Proof.
  Admitted.

Example exp_1 : exp dois dois = soma dois dois.
Proof.
  Admitted.

Example exp_2 : exp tres dois = soma (mult dois (mult dois dois)) um.
Proof.
  Admitted.

Example exp_3 : exp tres zero = um.
Proof.
  Admitted.

author: Gastd

repo: fptt

save_path: github-repos/coq/Gastd-fptt


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Register allocation. *)

Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import RTLtyping.
Require Import Kildall.
Require Import Locations.
Require Import Conventions.
Require Import Coloring.

(** * Liveness analysis over RTL *)

(** A register [r] is live at a point [p] if there exists a path
  from [p] to some instruction that uses [r] as argument,
  and [r] is not redefined along this path.
  Liveness can be computed by a backward dataflow analysis.
  The analysis operates over sets of (live) pseudo-registers. *)

Notation reg_live := Regset.add.
Notation reg_dead := Regset.remove.

Definition reg_option_live (or: option reg) (lv: Regset.t) :=
  match or with None => lv | Some r => reg_live r lv end.

Definition reg_sum_live (ros: reg + ident) (lv: Regset.t) :=
  match ros with inl r => reg_live r lv | inr s => lv end.

Fixpoint reg_list_live
             (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t :=
  match rl with
  | nil => lv
  | r1 :: rs => reg_list_live rs (reg_live r1 lv)
  end.

Fixpoint reg_list_dead
             (rl: list reg) (lv: Regset.t) {struct rl} : Regset.t :=
  match rl with
  | nil => lv
  | r1 :: rs => reg_list_dead rs (reg_dead r1 lv)
  end.

(** Here is the transfer function for the dataflow analysis.
  Since this is a backward dataflow analysis, it takes as argument
  the abstract register set ``after'' the given instruction,
  i.e. the registers that are live after; and it returns as result
  the abstract register set ``before'' the given instruction,
  i.e. the registers that must be live before.
  The general relation between ``live before'' and ``live after''
  an instruction is that a register is live before if either
  it is one of the arguments of the instruction, or it is not the result
  of the instruction and it is live after.
  However, if the result of a side-effect-free instruction is not
  live ``after'', the whole instruction will be removed later
  (since it computes a useless result), thus its arguments need not
  be live ``before''. *)

Definition transfer
            (f: RTL.function) (pc: node) (after: Regset.t) : Regset.t :=
  match f.(fn_code)!pc with
  | None =>
      Regset.empty
  | Some i =>
      match i with
      | Inop s =>
          after
      | Iop op args res s =>
          if Regset.mem res after then
            reg_list_live args (reg_dead res after)
          else
            after
      | Iload chunk addr args dst s =>
          if Regset.mem dst after then
            reg_list_live args (reg_dead dst after)
          else
            after
      | Istore chunk addr args src s =>
          reg_list_live args (reg_live src after)
      | Icall sig ros args res s =>
          reg_list_live args
           (reg_sum_live ros (reg_dead res after))
      | Itailcall sig ros args =>
          reg_list_live args (reg_sum_live ros Regset.empty)
      | Ibuiltin ef args res s =>
          reg_list_live args (reg_dead res after)
      | Icond cond args ifso ifnot =>
          reg_list_live args after
      | Ijumptable arg tbl =>
          reg_live arg after
      | Ireturn optarg =>
          reg_option_live optarg Regset.empty
      end
  end.

(** The liveness analysis is then obtained by instantiating the
  general framework for backward dataflow analysis provided by
  module [Kildall].  *)

Module RegsetLat := LFSet(Regset).
Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).

Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
  DS.fixpoint (successors f)  (transfer f) nil.

(** * Translation from RTL to LTL *)

Require Import LTL.

(** Each [RTL] instruction translates to an [LTL] instruction.
  The register assignment [assign] returned by register allocation
  is applied to the arguments and results of the RTL
  instruction.  Moreover, dead instructions and redundant moves
  are eliminated (turned into a [Lnop] instruction).
  Dead instructions are instructions without side-effects ([Iop] and
  [Iload]) whose result register is dead, i.e. whose result value
  is never used.  Redundant moves are moves whose source and destination
  are assigned the same location. *)

Definition is_redundant_move
    (op: operation) (args: list reg) (res: reg) (assign: reg -> loc) : bool :=
  match is_move_operation op args with
  | None => false
  | Some src => if Loc.eq (assign src) (assign res) then true else false
  end.

Definition transf_instr
         (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc)
         (pc: node) (instr: RTL.instruction) : LTL.instruction :=
  match instr with
  | Inop s =>
      Lnop s
  | Iop op args res s =>
      if Regset.mem res live!!pc then
        if is_redundant_move op args res assign then
          Lnop s
        else
          Lop op (List.map assign args) (assign res) s
      else
        Lnop s
  | Iload chunk addr args dst s =>
      if Regset.mem dst live!!pc then
        Lload chunk addr (List.map assign args) (assign dst) s
      else
        Lnop s
  | Istore chunk addr args src s =>
      Lstore chunk addr (List.map assign args) (assign src) s
  | Icall sig ros args res s =>
      Lcall sig (sum_left_map assign ros) (List.map assign args)
                (assign res) s
  | Itailcall sig ros args =>
      Ltailcall sig (sum_left_map assign ros) (List.map assign args)
  | Ibuiltin ef args res s =>
      Lbuiltin ef (List.map assign args) (assign res) s
  | Icond cond args ifso ifnot =>
      Lcond cond (List.map assign args) ifso ifnot
  | Ijumptable arg tbl =>
      Ljumptable (assign arg) tbl
  | Ireturn optarg =>
      Lreturn (option_map assign optarg)
  end.

Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
                      (assign: reg -> loc) : LTL.function :=
  LTL.mkfunction
     (RTL.fn_sig f)
     (List.map assign (RTL.fn_params f))
     (RTL.fn_stacksize f)
     (PTree.map (transf_instr f live assign) (RTL.fn_code f))
     (RTL.fn_entrypoint f).

(** The translation of a function performs liveness analysis,
  construction and coloring of the inference graph, and per-instruction
  transformation as described above. *)

Definition live0 (f: RTL.function) (live: PMap.t Regset.t) :=
  transfer f f.(RTL.fn_entrypoint) live!!(f.(RTL.fn_entrypoint)).

Open Scope string_scope.

Definition transf_function (f: RTL.function) : res LTL.function :=
  match type_function f with
  | Error msg => Error msg
  | OK env =>
    match analyze f with
    | None => Error (msg "Liveness analysis failure")
    | Some live =>
        match regalloc f live (live0 f live) env with
        | None => Error (msg "Incorrect graph coloring")
        | Some assign => OK (transf_fun f live assign)
        end
    end
  end.

Definition transf_fundef (fd: RTL.fundef) : res LTL.fundef :=
  AST.transf_partial_fundef transf_function fd.

Definition transf_program (p: RTL.program) : res LTL.program :=
  transform_partial_program transf_fundef p.

author: Ptival

repo: compcert-alias

save_path: github-repos/coq/Ptival-compcert-alias


text:
From mathcomp Require Import ssreflect ssrnat eqtype.
From deriving Require Import deriving.

Require Import type.

(* t_rect is the recursor automatically generated by Coq *)
Fail Definition t_indDef n := [indDef for t_rect n].

author: eponier

repo: compare-eq

save_path: github-repos/coq/eponier-compare-eq


text:
Require Export GeoCoq.Elements.OriginalProofs.proposition_23B.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_23C :
   forall A B C D E P,
   neq A B -> nCol D C E -> nCol A B P ->
   exists X Y, Out A B Y /\ CongA X A Y D C E /\ OS X P A B.
Proof.
intros.
assert (~ eq P A).
 {
 intro.
 assert (eq A P) by (conclude lemma_equalitysymmetric).
 assert (Col A B P) by (conclude_def Col ).
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists Q, (BetS P A Q /\ Cong A Q P A)) by (conclude lemma_extension);destruct Tf as [Q];spliter.
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (~ Col A B Q).
 {
 intro.
 assert (Col P A Q) by (conclude_def Col ).
 assert (Col Q A B) by (forward_using lemma_collinearorder).
 assert (Col Q A P) by (forward_using lemma_collinearorder).
 assert (neq A Q) by (forward_using lemma_betweennotequal).
 assert (neq Q A) by (conclude lemma_inequalitysymmetric).
 assert (Col A B P) by (conclude lemma_collinear4).
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists F G, (Out A B G /\ CongA F A G D C E /\ TS F A B Q)) by (conclude proposition_23B);destruct Tf as [F[G]];spliter.
let Tf:=fresh in
assert (Tf:exists J, (BetS F J Q /\ Col A B J /\ nCol A B F)) by (conclude_def TS );destruct Tf as [J];spliter.
assert (OS F P A B) by (conclude_def OS ).
close.
Qed.

End Euclid.

author: GeoCoq

repo: GeoCoq

save_path: github-repos/coq/GeoCoq-GeoCoq