Merge pull request #32 from Yag000/doc

Jfla doc

theories/extraction/UIML_extraction.v

@@ -5,7 +5,7 @@ Require Import ExtrOcamlBasic ExtrOcamlString.
 
 Require Import K.Interpolation.UIK_braga.
 Require Import KS_export.
-Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp ISL.Simp_env.
+Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp_env.
 
 
 
@@ -38,8 +38,8 @@ Definition isl_A v f := Af v f.
   Notable exception: (a ∨b) → c *)
 Definition isl_simp f := simp_form f.
 
-Definition isl_simplified_E v f := E_simplified v f.
-Definition isl_simplified_A v f := A_simplified v f.
+Definition isl_simplified_E p ψ := isl_simp (E p [ψ]).
+Definition isl_simplified_A p ψ := isl_simp (Af p (ψ)).
 
 Set Extraction Output Directory "extraction".
 

theories/iSL/DecisionProcedure.v

@@ -1,5 +1,11 @@
 Require Import ISL.Sequents ISL.SequentProps ISL.Order.
 
+(**
+  This file implements a decision procedure for iSL. There are two versions, with the same proof.
+  `Proof_tree_dec` computes a proof tree for the sequent, while `Provable_dec` only decides the provability
+  of the sequent.
+*)
+
 Global Instance proper_rm : Proper ((=) ==> (≡ₚ) ==> (≡ₚ)) rm.
 Proof.
 intros x y Heq. subst y.
@@ -21,7 +27,10 @@ induction l as [|x l].
     * right. simpl. intros z [Hz|Hz]; subst; try rewrite Heq; auto with *.
 Defined.
 
-(* This function computes a proof tree of a sequent, if there is one, or produces a proof that there is none *)
+(* This function computes a proof tree of a sequent, if there is one, or produces a proof that there is none.
+   The proof is performed by induction on the  well-ordering or pointed environments and tries to apply
+   all the sequent rules to reduce the weight of the environment.
+ *)
 Proposition Proof_tree_dec Γ φ :
   {_ : list_to_set_disj Γ ⊢ φ & True} + {forall H : list_to_set_disj  Γ ⊢ φ, False}.
 Proof.
@@ -35,12 +44,18 @@ remember (Γ, φ) as pe.
 replace Γ with pe.1 by now inversion Heqpe.
 replace φ with pe.2 by now inversion Heqpe. clear Heqpe Γ φ.
 revert pe.
+(* Induction on the  well-ordering of pointed environments *)
 refine  (@well_founded_induction _ _ wf_pointed_order _ _).
+
+(* Cleaning up the induction hypothesis *)
 intros (Γ& φ) Hind; simpl.
 assert(Hind' := λ Γ' φ', Hind(Γ', φ')). simpl in Hind'. clear Hind. rename Hind' into Hind.
 
+(* ExFalso *)
 case (decide (⊥ ∈ Γ)); intro Hbot.
 { left. eexists; trivial. apply elem_of_list_to_set_disj in Hbot. exhibit Hbot 0. apply ExFalso. }
+
+(* AndR *)
 assert(HAndR : {φ1 & {φ2 & φ = (And φ1 φ2)}} + {∀ φ1 φ2, φ ≠ (And φ1 φ2)}) by (destruct φ; eauto).
 destruct HAndR as [(φ1 & φ2 & Heq) | HAndR].
 { subst.
@@ -50,13 +65,17 @@ destruct HAndR as [(φ1 & φ2 & Heq) | HAndR].
     + right. intro Hp. apply AndR_rev in Hp. tauto.
   - right. intro Hp. apply AndR_rev in Hp. tauto.
 }
+
+(* Atom *)
 assert(Hvar : {p & φ = Var p & Var p ∈ Γ} + {∀ p, φ = Var p -> Var p ∈ Γ -> False}). {
   destruct φ. 2-6: right; auto with *.
   case (decide (Var v ∈ Γ)); intro Hin.
   - left. exists v; trivial.
   - right; auto with *. }
 destruct Hvar as [[p Heq Hp]|Hvar].
 { subst. left. eexists; trivial. apply elem_of_list_to_set_disj in Hp. exhibit Hp 0. apply Atom. }
+
+(* AndL *)
 assert(HAndL : {ψ1 & {ψ2 & (And ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (And ψ1 ψ2) ∈ Γ -> False}). {
   pose (fA := (fun θ => match θ with |And _ _ => true | _ => false end)).
   destruct (exists_dec fA Γ) as [(θ & Hin & Hθ) | Hf].
@@ -79,13 +98,17 @@ destruct HAndL as [(ψ1 & ψ2 & Hin)|HAndL].
    pose (difference_singleton (list_to_set_disj Γ) (And ψ1 ψ2)).
    peapply Hf'.
 }
+
+(* ImpR *)
 assert(HImpR : {φ1 & {φ2 & φ = (Implies φ1 φ2)}} + {∀ φ1 φ2, φ ≠ (Implies φ1 φ2)}) by (destruct φ; eauto).
 destruct HImpR as [(φ1 & φ2 & Heq) | HImpR].
 { subst.
   destruct (Hind (φ1 :: Γ) φ2) as [(Hp1&_) | H1]. order_tac.
   - left. eexists; trivial. apply ImpR. peapply Hp1.
   - right. intro Hf. apply H1. apply ImpR_rev in Hf. peapply Hf.
 }
+
+(* OrL *)
 assert(HOrL : {ψ1 & {ψ2 & (Or ψ1 ψ2) ∈ Γ}} + {∀ ψ1 ψ2, (Or ψ1 ψ2) ∈ Γ -> False}). {
   pose (fA := (fun θ => match θ with |Or _ _ => true | _ => false end)).
   destruct (exists_dec fA Γ) as [(θ & Hin & Hθ) | Hf].
@@ -111,6 +134,8 @@ destruct HOrL as [(ψ1 & ψ2 & Hin)|HOrL].
          }
         apply OrL_rev in Hf''. apply Hf. peapply Hf''.1.
 }
+
+(* ImpLVar *)
 assert(HImpLVar : {p & {ψ & Var p ∈ Γ /\ (Implies (Var p) ψ) ∈ Γ}} + 
                                  {∀ p ψ, Var p ∈ Γ -> (Implies (Var p) ψ) ∈ Γ -> False}). {
   pose (fIp :=λ p θ, match θ with | Implies (Var q) _ => if decide (p = q) then true else false | _ => false end).
@@ -144,6 +169,8 @@ destruct HImpLVar as [[p [ψ [Hinp Hinψ]]]|HImpLVar].
      rw (symmetry (difference_singleton _ _ Hinψ)) 0.
      exact Hf'.
 }
+
+(* ImpLAnd *)
 assert(HImpLAnd : {φ1 & {φ2 & {φ3 &  (Implies (And φ1 φ2) φ3) ∈ Γ}}} +
                                  {∀ φ1 φ2 φ3, (Implies (And φ1 φ2) φ3) ∈ Γ -> False}). {
     pose (fII := (fun θ => match θ with |Implies (And _ _) _ => true | _ => false end)).
@@ -163,6 +190,8 @@ destruct HImpLAnd as [(φ1&φ2&φ3&Hin)|HImpLAnd].
      apply ImpLAnd_rev.
      rw (symmetry (difference_singleton _ _ Hin)) 0. exact Hf'.
 }
+
+(* ImpLOr *)
 assert(HImpLOr : {φ1 & {φ2 & {φ3 &  (Implies (Or φ1 φ2) φ3) ∈ Γ}}} +
                                  {∀ φ1 φ2 φ3, (Implies (Or φ1 φ2) φ3) ∈ Γ -> False}). {
     pose (fII := (fun θ => match θ with |Implies (Or _ _) _ => true | _ => false end)).
@@ -183,7 +212,10 @@ destruct HImpLOr as [(φ1&φ2&φ3&Hin)|HImpLOr].
      apply ImpLOr_rev.
      rw (symmetry (difference_singleton _ _ Hin)) 0. exact Hf'.
 }
+
 (* non invertible right rules *)
+
+(* OrR1 *)
 assert(HOrR1 : {φ1 & {φ2 & {Hp : (list_to_set_disj Γ ⊢ φ1) & φ = (Or φ1 φ2)}}} +
                        {∀ φ1 φ2, ∀ (H : list_to_set_disj Γ ⊢ φ1), φ = (Or φ1 φ2) -> False}).
 {
@@ -204,6 +236,8 @@ assert(HOrR2 : {φ1 & {φ2 & {Hp : (list_to_set_disj Γ ⊢ φ2) & φ = (Or φ1
   }
   all: right; auto with *.
 }
+
+(* OrR2 *)
 destruct HOrR2 as [(φ1 & φ2 & Hp & Heq)| HOrR2 ].
 { subst. left. eexists; trivial. apply OrR2, Hp. }
 assert(HBoxR : {φ' & {Hp : (⊗ (list_to_set_disj Γ) • □ φ' ⊢ φ') & φ = (□ φ')}} +
@@ -217,6 +251,8 @@ assert(HBoxR : {φ' & {Hp : (⊗ (list_to_set_disj Γ) • □ φ' ⊢ φ') & φ
   }
   all: right; auto with *.
 }
+
+(* BoxR *)
 destruct HBoxR as [(φ' & Hp & Heq)| HBoxR ].
 { left. subst. eexists; trivial. apply BoxR, Hp. }
 assert(Hempty: ∀ (Δ : env) φ,((Δ • φ) = ∅) -> False).
@@ -225,7 +261,10 @@ assert(Hempty: ∀ (Δ : env) φ,((Δ • φ) = ∅) -> False).
   unfold base.empty in *.
   rewrite <- Heq, union_mult, singleton_mult_in in Hm by trivial. lia.
 }
+
 (* non invertible left rules *)
+
+(* ImpLImp *)
 assert(HImpLImp : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ -> {φ1 & {φ2 & {φ3 &{H2312 : ((list_to_set_disj (rm (Implies (Implies φ1 φ2) φ3) Γ) • (Implies φ2 φ3)) ⊢ (Implies φ1 φ2))
                                           & {H3: (list_to_set_disj (rm (Implies (Implies φ1 φ2) φ3) Γ) • φ3 ⊢ φ) & (Implies (Implies φ1 φ2) φ3) ∈ Γ2}}}}} +
     {∀ φ1 φ2 φ3 (_ : (list_to_set_disj (rm (Implies (Implies φ1 φ2) φ3) Γ) • (Implies φ2 φ3)) ⊢ (Implies φ1 φ2))
@@ -263,7 +302,8 @@ destruct (HImpLImp Γ [] (app_nil_l _)) as [(φ1 & φ2 & φ3 & Hp1 & Hp2 & Hin)|
   left. eexists; trivial. exhibit Hin 0. rw (list_to_set_disj_rm Γ(Implies (Implies φ1 φ2) φ3)) 1.
   apply ImpLImp; assumption.
 } 
-(* ImpBox *)
+
+(* ImpLBox *)
 assert(HImpLBox : ∀Γ2 Γ1, Γ1 ++ Γ2 = Γ -> {φ1 & {φ2 & {H2312 : ((⊗(list_to_set_disj ((rm (Implies (□ φ1) φ2) Γ))) • □ φ1 • φ2) ⊢φ1)
                                           & {H3: (list_to_set_disj (rm (Implies (□ φ1) φ2) Γ) • φ2 ⊢ φ) & (Implies (□ φ1) φ2) ∈ Γ2}}}} +
     {∀ φ1 φ2 (_ : ((⊗ (list_to_set_disj ((rm (Implies (□ φ1) φ2) Γ))) • □ φ1 • φ2) ⊢φ1))
@@ -303,6 +343,8 @@ destruct (HImpLBox Γ [] (app_nil_l _)) as [(φ1 & φ2 & Hp1 & Hp2 & Hin)|HfImpL
   left. eexists; trivial. exhibit Hin 0. rw (list_to_set_disj_rm Γ(Implies (□ φ1) φ2)) 1.
   apply ImpBox; assumption.
 }
+
+(* All the sequent rules have been applied *)
 clear Hind HImpLImp HImpLBox.
 right.
 Ltac eqt := match goal with | H : (_ • ?φ) = list_to_set_disj ?Γ |- _ =>
@@ -322,7 +364,9 @@ intro Hp. inversion Hp; subst; try eqt; eauto 2.
 Defined.
 
 
-(* This function decides whether a sequent is provable *)
+(* This function decides whether a sequent is provable.
+   The proof is the same as `Proof_tree_dec`.
+ *)
 Proposition Provable_dec Γ φ :
   (exists _ : list_to_set_disj Γ ⊢ φ, True) + (forall H : list_to_set_disj  Γ ⊢ φ, False).
 Proof.

theories/iSL/Optimizations.v

@@ -29,7 +29,9 @@ Qed.
 
 Global Hint Resolve top_provable : proof.
 
-(* decides whether one formula entails the other or not ; in the latter case return Eq *)
+(* Decides whether one formula entails the other or not ; in the latter case return Eq.
+   It uses the decision procedure for iSL defined at `DecisionProcedure.v`
+*)
 Definition obviously_smaller (φ : form) (ψ : form) :=
   if [φ] ⊢? ψ then Lt
   else if [ψ] ⊢? φ then Gt
@@ -46,7 +48,6 @@ match obviously_smaller φ ψ with
 Lemma occurs_in_choose_conj v φ ψ : occurs_in v (choose_conj φ ψ) -> occurs_in v φ \/ occurs_in v ψ.
 Proof. unfold choose_conj; destruct obviously_smaller; simpl; intros; tauto. Qed.
 
-
 Definition make_conj φ ψ := 
 match ψ with
   | ψ1 ∧ ψ2 =>
@@ -125,7 +126,6 @@ Qed.
 
 (* "lazy" implication, which produces a potentially simpler, equivalent formula *)
 
-(* Same as `simp_ors` but for nested implications. *)
 Definition choose_impl φ ψ:=
      if decide (obviously_smaller φ ψ = Lt) then ⊤
      else if decide (obviously_smaller φ ⊥ = Lt) then ⊤
@@ -688,7 +688,6 @@ Qed.
 (** ** Generalized invertibility of AndR *)
 
 
-
 (** ** Generalized AndR *)
 
 Lemma conjunction_R1 Γ Δ : (forall φ, φ ∈ Δ -> Γ  ⊢ φ) -> (Γ  ⊢ ⋀ Δ).
@@ -749,7 +748,10 @@ Qed.
 (* TODO move up *)
 (** * Correctness of optimizations 
 
-To make the definitions of the propositional quantifiers that we extract from the Coq definition more readable, we introduced functions "make_impl", "make_conj" and "make_disj" in Environments.v which perform obvious simplifications such as reducing φ ∧ ⊥ to ⊥ and φ ∨ ⊥ to φ. The following results show that the definitions of these functions are correct, in the sense that it does not make a difference for provability of a sequent whether one uses the literal conjunction, disjunction, and implication, or its optimized version. *)
+To make the definitions of the propositional quantifiers that we extract from the Coq definition more readable, we introduced the
+functions "make_impl", "make_conj" and "make_disj" in Optimizations.v which perform obvious simplifications such as reducing φ ∧ ⊥
+to ⊥ and φ ∨ ⊥ to φ. The following results show that the definitions of these functions are correct, in the sense that it does not 
+make a difference for provability of a sequent whether one uses the literal conjunction, disjunction, and implication, or its optimized version. *)
 
 (* TODO: suitable name *)
 Lemma tautology_cut {Γ} {φ ψ θ : form} : Γ • (φ → ψ) ⊢ θ -> (φ ≼ ψ) -> Γ ⊢ θ.