Move ghc to naming schema Proofs.<modulename>

not doing it to `containers` yet, as there is a `Set.v` and
`SetProofs.v` file in  `theories`.

Presumably, `Set.v` should not be in `Proofs.` but rather something else
(`Wrapped.`)?

examples/ghc/theories/BaseLemmas.v → examples/ghc/theories/Base.v

@@ -5,7 +5,7 @@ Require Import Proofs.GHC.List.
 
 Require Import Coq.Lists.List.
 
-Require Import GhcProofs.Tactics.
+Require Import Proofs.GhcTactics.
 
 Import ListNotations.
 

examples/ghc/theories/CoreLemmas.v → examples/ghc/theories/Core.v

@@ -4,8 +4,8 @@ Require Import CoreFVs.
 
 Require Import Proofs.GHC.Base.
 Require Import Proofs.GHC.List.
-Require Import GhcProofs.Tactics.
-Require Import GhcProofs.BaseLemmas.
+Require Import Proofs.GhcTactics.
+Require Import Proofs.Base.
 
 Require Import Coq.Logic.FunctionalExtensionality.
 Require Import Coq.Lists.List.
@@ -183,4 +183,4 @@ Proof.
     replace (n - 0) with n; auto.
     apply IHn; auto.
     omega.
-Qed.
+Qed.

examples/ghc/theories/CoreFVsLemmas.v → examples/ghc/theories/CoreFVs.v

@@ -5,10 +5,10 @@ Require Import Core.
 
 Require Import Coq.Lists.List.
 
-Require Import GhcProofs.Tactics.
-Require Import GhcProofs.BaseLemmas.
-Require Import GhcProofs.CoreInduct.
-Require Import GhcProofs.CoreLemmas.
+Require Import Proofs.GhcTactics.
+Require Import Proofs.Base.
+Require Import Proofs.CoreInduct.
+Require Import Proofs.Core.
 
 Set Bullet Behavior "Strict Subproofs".
 

examples/ghc/theories/CoreInduct.v

@@ -3,8 +3,8 @@ Require Import Coq.Lists.List.
 Import ListNotations.
 Require Import Psatz.
 
-Require Import GhcProofs.Tactics.
-Require Import GhcProofs.CoreLemmas.
+Require Import Proofs.GhcTactics.
+Require Import Proofs.Core.
 
 
 Set Bullet Behavior "Strict Subproofs".

examples/ghc/theories/CoreSubstInvariants.v

@@ -17,7 +17,7 @@ Import GHC.Base.Notations.
 Import Coq.Logic.FunctionalExtensionality.
 
 Require Proofs.GHC.Base.
-Require GhcProofs.CoreInduct.
+Require Proofs.CoreInduct.
 
 
 Set Bullet Behavior "Strict Subproofs".

examples/ghc/theories/ExitifyProofs.v → examples/ghc/theories/Exitify.v

@@ -16,20 +16,20 @@ Require Import Coq.Logic.FunctionalExtensionality.
 
 Set Bullet Behavior "Strict Subproofs".
 
-Require Import GhcProofs.BaseLemmas.
-Require Import GhcProofs.JoinPointInvariants.
-Require Import GhcProofs.ScopeInvariant.
-Require Import GhcProofs.StateLogic.
-Require Import GhcProofs.CoreInduct.
-Require Import GhcProofs.Forall.
-Require Import GhcProofs.CoreLemmas.
-Require Import GhcProofs.CoreFVsLemmas.
-Require Import GhcProofs.Tactics.
-Require Import GhcProofs.NCore.
-Require Import GhcProofs.VectorUtils.
-Require Import GhcProofs.VarLemmas.
-Require Import GhcProofs.VarSet.
-Require Import GhcProofs.Unique.
+Require Import Proofs.Base.
+Require Import Proofs.JoinPointInvariants.
+Require Import Proofs.ScopeInvariant.
+Require Import Proofs.StateLogic.
+Require Import Proofs.CoreInduct.
+Require Import Proofs.Forall.
+Require Import Proofs.Core.
+Require Import Proofs.CoreFVs.
+Require Import Proofs.GhcTactics.
+Require Import Proofs.NCore.
+Require Import Proofs.VectorUtils.
+Require Import Proofs.Var.
+Require Import Proofs.VarSet.
+Require Import Proofs.Unique.
 
 Close Scope Z_scope.
 

examples/ghc/theories/Forall.v

@@ -24,4 +24,4 @@ Proof.
   unfold id.
   rewrite Forall_map.
   reflexivity.
-Qed.
+Qed.

examples/ghc/theories/JoinPointInvariants.v

@@ -10,8 +10,8 @@ Require Import Psatz.
 
 Import ListNotations.
 
-Require Import GhcProofs.Forall.
-Require Import GhcProofs.CoreLemmas.
+Require Import Proofs.Forall.
+Require Import Proofs.Core.
 
 Set Bullet Behavior "Strict Subproofs".
 

examples/ghc/theories/NCore.v

@@ -8,7 +8,7 @@ Require Import Coq.Bool.Bool.
 Require Import Coq.NArith.BinNat.
 Require Import Psatz.
 
-Require Import GhcProofs.VectorUtils.
+Require Import Proofs.VectorUtils.
 
 Import ListNotations.
 

examples/ghc/theories/ScopeInvariant.v

@@ -5,9 +5,9 @@ Require Import CoreUtils.
 Require Import Coq.Lists.List.
 Import ListNotations.
 
-Require Import GhcProofs.Forall.
-Require Import GhcProofs.CoreFVsLemmas.
-Require Import GhcProofs.VarSet.
+Require Import Proofs.Forall.
+Require Import Proofs.CoreFVs.
+Require Import Proofs.VarSet.
 
 Set Bullet Behavior "Strict Subproofs".
 

examples/ghc/theories/VarSet.v

@@ -16,11 +16,11 @@ Open Scope Z_scope.
 
 Set Bullet Behavior "Strict Subproofs".
 
-Require Import GhcProofs.Tactics.
-Require Import GhcProofs.BaseLemmas.
-Require Import GhcProofs.ContainerAxioms.
-Require Import GhcProofs.Unique.
-Require Import GhcProofs.VarLemmas.
+Require Import Proofs.GhcTactics.
+Require Import Proofs.Base.
+Require Import Proofs.ContainerAxioms.
+Require Import Proofs.Unique.
+Require Import Proofs.Var.
 
 Require Import IntSetProofs.
 (* Require Import IntMapProofs. *)

examples/ghc/theories/_CoqProject

@@ -1,4 +1,4 @@
--Q . GhcProofs
+-Q . Proofs
 -R ../../../base ""
 -Q ../../../base-thy  Proofs
 -Q ../../ghc/lib ""
@@ -9,17 +9,17 @@ ScopeInvariant.v
 JoinPointInvariants.v
 # JoinPointInvariantsInductive.v
 CoreInduct.v
-ExitifyProofs.v
+Exitify.v
 CoreSubstInvariants.v
 StateLogic.v
-Tactics.v
+GhcTactics.v
 Forall.v
-CoreLemmas.v
+Core.v
 NCore.v
 VectorUtils.v
-CoreFVsLemmas.v
-BaseLemmas.v
+CoreFVs.v
+Base.v
 VarSet.v
 Unique.v
 ContainerAxioms.v
-VarLemmas.v
+Var.v