commit 4cddd6b0c91491e88eb675d18ed61b31953ab8cc
Author: Noah Diewald <noah@diewald.me>
Date:   Thu May 2 11:26:54 2019 -0400

    first commit

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..6c7a856
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+# nabese
diff --git a/SimpleFragment.v b/SimpleFragment.v
new file mode 100644
index 0000000..edbbead
--- /dev/null
+++ b/SimpleFragment.v
@@ -0,0 +1,246 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String.
+Import ListNotations.
+
+Open Scope type_scope.
+Open Scope string_scope.
+
+(* First we define lexes, which are building blocks for lexemes. These
+are not lexemes themselves because we require additional structure to
+develop a notion of derivational relationships. *)
+
+Inductive lex : Set :=
+| OS : lex (* father *)
+| NESHNABÉ : lex (* person *)
+| BIWABEK : lex (* metal *)
+| MOWECH : lex (* feces *)
+| BAGJÉʔGEN : lex. (* pool cue *)
+
+(* Here we define the only derivational relationship that we are
+concerned with for this fragment, IJ, which relates lexes to a lexeme
+that is related by the function c to the class appropriate to
+inalienably possessed nouns. *)
+
+Inductive rel : Set :=
+| IJ : rel. (* fellow *)
+
+(* Lexemes are either simple, in the case of root or have a
+relationship to a class of likewise derived lexemes in the case of
+cmplx. *)
+
+Inductive lexeme : Type :=
+| root (l : lex)
+| cmplx (r : rel) (l : lex).
+
+(* The type mm is for atoms used in m-categories or mcats, which are
+lists of mms. Here this is somewhat redundant because our fragment is
+so simple. *)
+
+Inductive mm : Set :=
+| free : mm
+| freem : mm
+| bound : mm
+| nposs : mm.
+
+(* I define fclasses that are not used in this fragment. These are
+related to lexemes by the function c. *)
+
+Inductive fclass : Set :=
+| long : fclass
+| short : fclass
+| nosuffix : fclass
+| msuffix : fclass
+| LN : fclass
+| LM : fclass
+| SN : fclass
+| SM : fclass
+| LNM : fclass
+| LSN : fclass
+| LSM : fclass
+| SNM : fclass
+| LSNM : fclass
+| none : fclass. (* This will exist outside the order. *)
+
+(* As stated above, mcat is a list of mms. An mform is a string. *)
+
+Definition mcat := list mm.
+Definition mform := string.
+
+(* An mtrip is the data structure used to define Fentrys *)
+
+Definition mtrip := mcat * mform * lexeme.
+
+(* Note that the check below demonstrates why simply saying that we're
+working with mtrips is not good enough. Non-grammatical triples
+check. We need to be able to specify which are legal triples. *)
+
+Check ([ SNM ] , "walk" , root OS).
+
+(* To solve this I define a predicate Fentry, the use of which will be
+seen below. Essentially, only grammatical mtrips will be Fentrys. *)
+
+Axiom Fentry : mtrip -> Prop.
+
+(* lem is the order over mcats. The axioms below define it as an
+order. *)
+
+Axiom lem : mcat -> mcat -> Prop.
+Axiom lem_refl : forall x : mcat, lem x x.
+Axiom lem_antisym : forall x y : mcat, lem x y -> lem y x -> x = y.
+Axiom lem_trans : forall x y z : mcat, lem x y -> lem y z -> lem x z.
+
+(* The order is not natural. We define, explicitly, the relation. *)
+
+Axiom free_lem_bound : lem [ free ] [ bound ].
+Axiom free_lem_freem : lem [ free ] [ freem ].
+
+(* lef is the order over fclasses. The axioms below define it as an
+order. *)
+
+Axiom lef : fclass -> fclass -> Prop.
+Axiom lef_refl : forall x : fclass, lef x x.
+Axiom lef_antisym : forall x y : fclass, lef x y -> lef y x -> x = y.
+Axiom lef_trans : forall x y z : fclass, lef x y -> lef y z -> lef x z.
+
+(* The order is not natural. We define, explicitly, the relation. *)
+
+Axiom ln_lef_long : lef LN long.
+Axiom lm_lef_long : lef LM long.
+Axiom ln_lef_nosuffix : lef LN nosuffix.
+Axiom sn_lef_nosuffix : lef SN nosuffix.
+Axiom lm_lef_msuffix : lef LM msuffix.
+Axiom sm_lef_msuffix : lef SM msuffix.
+Axiom sn_lef_short : lef SN short.
+Axiom sm_lef_short : lef SM short.
+Axiom lnm_lef_ln : lef LNM LN.
+Axiom lsn_lef_ln : lef LSN LN.
+Axiom lnm_lef_lm : lef LNM LM.
+Axiom lsm_lef_lm : lef LSM LM.
+Axiom lsn_lef_sn : lef LSN SN.
+Axiom snm_lef_sn : lef SNM SN.
+Axiom lsm_lef_sm : lef LSM SM.
+Axiom snm_lef_sm : lef SNM SM.
+Axiom lsnm_lef_lnm : lef LSNM LNM.
+Axiom lsnm_lef_lsm : lef LSNM LSM.
+
+(* Below we define c which relates lexemes to their fclass. We assume
+that only cmplx IJ NESHNABÉ will have an fclass that allows for the
+derivation from root NESHNABÉ as this is the only attested lexeme for
+that derivation among the lexemes defined. *)
+
+Definition c (l:lexeme) : fclass :=
+  match l with
+  | root OS => SN
+  | root NESHNABÉ => LM
+  | root BIWABEK => LSM (* We'd predict LSNM but these are attested. *)
+  | root BAGJÉʔGEN => SNM (* The same as above. *)
+  | root MOWECH => LSNM (* There are missing forms here too. *)
+  | cmplx IJ lx => match lx with
+                   | NESHNABÉ => SN
+                   | _ => none
+                   end
+  end.
+
+(* Below I define the form building functions. These ignore the
+intricacies of providing correct surface forms as a simplification and
+due to a lack of the specification of a phonological interface. *)
+
+Definition suffix_m (s:mform) : mform :=
+  s ++ "m".
+
+Definition prefix_n (s:mform) : mform :=
+  "n" ++ s.
+
+Definition prefix_ned (s:mform) : mform :=
+  "ned" ++ s.
+
+Definition prefix_ij (s:mform) : mform :=
+  "ij" ++ s.
+
+(* These are definitions of basic stems for the lexemes above. Note
+that I define the mtrips first and then specify that they are
+Fentrys. *)
+
+Definition mowech_free := ([ free ], "mowech", root MOWECH) : mtrip.
+
+Definition os_bound := ([ bound ], "os", root OS) : mtrip.
+
+Axiom f_mowech_free : Fentry mowech_free.
+
+(* f_m is the rule for specifying that... *)
+
+Axiom f_m : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ freem ]) -> (lef (c (snd mt)) msuffix) -> Fentry ([ bound ], suffix_m (snd (fst mt)), (snd mt)).
+
+Axiom f_n : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ bound ]) -> (lef (c (snd mt)) short) -> Fentry ([ nposs ], prefix_n (snd (fst mt)), (snd mt)).
+
+Axiom f_ned : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ bound ]) -> (lef (c (snd mt)) long) -> Fentry ([ nposs ], prefix_ned (snd (fst mt)), (snd mt)).
+
+Definition glex (l:lexeme) :=
+  match l with
+  | root lx => lx
+  | cmplx _ lx => lx
+  end.
+  
+Axiom f_ij : forall (mt : mtrip), (Fentry mt) -> (lem (fst (fst mt)) [ freem ]) -> (lef (c (snd mt)) msuffix) -> Fentry ([ bound ], prefix_ij (snd (fst mt)), cmplx IJ (glex (snd mt))).
+
+Lemma walk_base_is_fentry:
+  Fentry mowech_free.
+Proof.
+  apply f_mowech_free.
+Qed.
+
+Lemma mowech_free_is_free:
+  lem (fst (fst mowech_free)) [ free ].
+Proof.
+  simpl.
+  apply lem_refl.
+Qed.
+
+Lemma mowech_free_is_LSNM:
+  lef (c (snd mowech_free)) LSNM.
+Proof.
+  simpl.
+  apply lef_refl.
+Qed.
+
+Lemma LM_is_msuffix:
+  lef LM msuffix.
+Proof.
+  apply lm_lef_msuffix.  
+Qed.
+
+Lemma LNM_is_msuffix:
+  lef LNM msuffix.
+Proof.
+  assert (H1 : lef LNM LM).
+  { apply lnm_lef_lm. }
+  assert (H2 : lef LM msuffix).
+  { apply lm_lef_msuffix. }
+  apply (lef_trans LNM LM msuffix H1 H2).
+Qed.
+
+Lemma mowech_free_is_msuffix:
+  lef (c (snd mowech_free)) msuffix.
+Proof.
+  simpl.
+  assert (H1 : lef LSNM LNM).
+  { apply lsnm_lef_lnm. }
+  assert (H2 : lef LNM msuffix).
+  { exact LNM_is_msuffix. }
+  apply (lef_trans LSNM LNM msuffix H1 H2).
+Qed.
+
+Example test_f_m:
+  Fentry ([ bound ], "mowechm", root MOWECH).
+Proof.
+  assert (H1 : lem [ free ] [ freem ]).
+  { apply free_lem_freem. }
+  assert (H2 : lef LSNM msuffix).
+  { exact mowech_free_is_msuffix. }
+  apply (f_m mowech_free).
+  exact f_mowech_free.
+  simpl.
+  assumption.
+  simpl.
+  assumption.
+Qed.