c_True is trivial; c_and is pair; c_or is sum

FStarLang · nikswamy · Feb 18, 2022 · Feb 16, 2022 · Feb 16, 2022 · Feb 16, 2022
commit a5cb4ee0d7e0a82ef85712f967fbdf95cb5354a5
diff --git a/examples/native_tactics/Tutorial.fst b/examples/native_tactics/Tutorial.fst
@@ -102,7 +102,7 @@ and you can simply think of the type `squash phi` as the type of irrelevant
 proofs of `phi`. We call goals that are squashed ``irrelevant''.
 
 > For experts: You might notice that `True` is already a squash (of
-> `c_True`), so this seems useless. In this case it is, but we squash
+> `trivial`), so this seems useless. In this case it is, but we squash
 > nevertheless for consistency since this might be not so.
 
 A tactic is not required to completely prove an assertion, and can leave

diff --git a/examples/paradoxes/PropositionalExtensionalityInconsistent.fst b/examples/paradoxes/PropositionalExtensionalityInconsistent.fst
@@ -61,7 +61,7 @@ let predExt_Type =
             (ensures (p1 == p2))
 let predExt_Type_inconsistent (ax:predExt_Type)
   : Lemma False
-  = let p1 : predicate int = fun n -> c_True in
+  = let p1 : predicate int = fun n -> trivial in
     let p2 : predicate int = fun n -> unit in
     ax int p1 p2
 
@@ -78,6 +78,6 @@ let predExt_ss =
             (ensures (p1 == p2))
 let predExt_ss_inconsistent (ax:predExt_ss)
   : Lemma False
-  = let p1 : predicate_ss int = fun n -> c_True in
+  = let p1 : predicate_ss int = fun n -> trivial in
     let p2 : predicate_ss int = fun n -> unit in
     ax int p1 p2
diff --git a/examples/tactics/Tutorial.fst b/examples/tactics/Tutorial.fst
@@ -93,7 +93,7 @@ let ex2 () =
 /// .. note::
 ///
 ///    For experts: You might notice that ``True`` is already a squash (of
-///    ``c_True``), so this seems useless. In this case it is, but we squash
+///    ``trivial``), so this seems useless. In this case it is, but we squash
 ///    nevertheless for consistency since this might be not so.
 
 /// A tactic is not required to completely prove an assertion, and can leave

diff --git a/src/ocaml-output/FStar_Parser_Const.ml b/src/ocaml-output/FStar_Parser_Const.ml
diff --git a/src/ocaml-output/FStar_Tests_Unif.ml b/src/ocaml-output/FStar_Tests_Unif.ml
diff --git a/src/ocaml-output/FStar_TypeChecker_TcInductive.ml b/src/ocaml-output/FStar_TypeChecker_TcInductive.ml
diff --git a/src/parser/FStar.Parser.Const.fs b/src/parser/FStar.Parser.Const.fs
@@ -104,7 +104,7 @@ let magic_lid  = pconst "magic"
 let has_type_lid = pconst "has_type"
 
 (* Constructive variants *)
-let c_true_lid      = pconst "c_True"
+let c_true_lid      = pconst "trivial"
 let empty_type_lid  = pconst "empty"
 let c_and_lid       = pconst "pair"
 let c_or_lid        = pconst "sum"

diff --git a/src/typechecker/FStar.TypeChecker.TcInductive.fs b/src/typechecker/FStar.TypeChecker.TcInductive.fs
@@ -780,7 +780,7 @@ let check_inductive_well_typedness (env:env_t) (ses:list<sigelt>) (quals:list<qu
 (******************************************************************************)
 
 //for these types we don't generate projectors, discriminators, and hasEq axioms
-let early_prims_inductives = [ "empty"; "c_True"; "equals"; "tuple2"; "sum" ]
+let early_prims_inductives = [ "empty"; "trivial"; "equals"; "pair"; "sum" ]
 
 let mk_discriminator_and_indexed_projectors iquals                   (* Qualifiers of the envelopping bundle    *)
                                             (attrs:list<attribute>)  (* Attributes of the envelopping bundle    *)

diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected
@@ -3,9 +3,9 @@ NegativeTests.False.fst(23,13-23,33): (Error 19) assertion failed; The SMT solve
 >>]
 >> Got issues: [
 NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum (*?u1*) _ Prims.l_True"
-NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.c_True Prims.l_True"
+NegativeTests.False.fst(30,18-30,40): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Left (Prims.T)" has type "Prims.sum Prims.trivial Prims.l_True"
 NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True (*?u6*) _"
-NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.c_True"
+NegativeTests.False.fst(30,41-30,63): (Error 12) Expected type "Prims.l_True \/ Prims.l_True"; but "Prims.Right (Prims.T)" has type "Prims.sum Prims.l_True Prims.trivial"
 >>]
 NegativeTests.False.fst(21,4-21,7): (Warning 240) Admitting NegativeTests.False.bar without a definition
 NegativeTests.False.fst(28,4-28,10): (Warning 240) Admitting NegativeTests.False.absurd without a definition

diff --git a/tests/micro-benchmarks/NormVsSMT.fst b/tests/micro-benchmarks/NormVsSMT.fst
@@ -19,8 +19,8 @@ let _ = assert_norm (True /\ True)
 let _ = assert_norm (True \/ True)
 
 (* These fail, and probably shouldn't, but it's not too worrysome *)
-(* let _ = assert (c_and True True) *)
-(* let _ = assert (c_and c_True c_True) *)
+(* let _ = assert (pair True True) *)
+(* let _ = assert (pair trivial trivial) *)
 
 (* This fails after removing t_valid, c.f. 5ac0bd96d *)
 (* val l1 : (a : Type) -> Lemma (a ==> squash a) *)

diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst
@@ -102,7 +102,7 @@ let stronger_markovs_principle_prop (p: (nat -> GTot prop))
 (** A proof for squash p can be eliminated to get p in the Ghost effect *)
 
 let elim_squash (#p:Type u#a) (s:squash p) : GTot p =
-  let uu : squash (x:p & squash c_True) =
+  let uu : squash (x:p & squash trivial) =
     bind_squash s (fun x -> return_squash (| x, return_squash T |)) in
   give_proof (return_squash uu);
-  indefinite_description_ghost p (fun _ -> squash c_True)
+  indefinite_description_ghost p (fun _ -> squash trivial)
diff --git a/ulib/fs/prims.fs b/ulib/fs/prims.fs
@@ -69,25 +69,25 @@ let uu___is_Left = function Left _ -> true | Right _ -> false
 
 let uu___is_Right = function Left _ -> false | Right _ -> true
 
-type (' p, ' q) tuple2 =
-| Mktuple2 of ' p * ' q
+type (' p, ' q) pair =
+| Pair of ' p * ' q
 
-type (' p, ' q) l_and = ('p, 'q) tuple2 squash
+type (' p, ' q) l_and = ('p, 'q) pair squash
 
-let uu___is_Mktuple2 _ = true
+let uu___is_Pair _ = true
 
 
-type c_True =
+type trivial =
   | T
 
-type l_True = c_True squash
+type l_True = trivial squash
 
 let uu___is_T _ = true
 
-type c_False = unit
+type empty = unit
 (*This is how Coq extracts Inductive void := . Our extraction needs to be fixed to recognize when there
        are no constructors and generate this type abbreviation*)
-type l_False = c_False squash
+type l_False = empty squash
 
 type (' p, ' q) l_imp = ('p -> 'q) squash
 

diff --git a/ulib/ml/prims.ml b/ulib/ml/prims.ml
@@ -23,9 +23,9 @@ type bool = bool'
 type empty = unit
 (*This is how Coq extracts Inductive void := . Our extraction needs to be fixed to recognize when there
        are no constructors and generate this type abbreviation*)
-type c_True =
+type trivial =
   | T
-let (uu___is_T : c_True -> bool) = fun projectee  -> true
+let (uu___is_T : trivial -> bool) = fun projectee  -> true
 type nonrec unit = unit
 type 'Ap squash = unit
 type 'Ap auto_squash = unit
@@ -38,29 +38,29 @@ let uu___is_Refl : 'Aa . 'Aa -> 'Aa -> ('Aa,unit,unit) equals -> bool =
 type ('Aa,'Ax,'Ay) eq2 = unit
 type ('Aa,'Ab,'Ax,'Ay) op_Equals_Equals_Equals = unit
 type 'Ab b2t = unit
-type ('Ap,'Aq) tuple2 =
-  | Mktuple2 of 'Ap * 'Aq
-let uu___is_Mktuple2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> bool =
+type ('Ap,'Aq) pair =
+  | Pair of 'Ap * 'Aq
+let uu___is_Pair : 'Ap 'Aq . ('Ap,'Aq) pair -> bool =
   fun projectee  -> true
-let __proj__Mktuple2__item___1 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Ap =
-  fun projectee  -> match projectee with | Mktuple2 (_0,_1) -> _0
-let __proj__Mktuple2__item___2 : 'Ap 'Aq . ('Ap,'Aq) tuple2 -> 'Aq =
-  fun projectee  -> match projectee with | Mktuple2 (_0,_1) -> _1
+let __proj__Pair__item___1 : 'Ap 'Aq . ('Ap,'Aq) pair -> 'Ap =
+  fun projectee  -> match projectee with | Pair (_0,_1) -> _0
+let __proj__Pair__item___2 : 'Ap 'Aq . ('Ap,'Aq) pair -> 'Aq =
+  fun projectee  -> match projectee with | Pair (_0,_1) -> _1
 type ('Ap,'Aq) l_and = unit
 type ('Ap,'Aq) sum =
   | Left of 'Ap
   | Right of 'Aq
-let uu___is_Left : 'Ap 'Aq . ('Ap,'Aq) either -> bool =
+let uu___is_Left : 'Ap 'Aq . ('Ap,'Aq) sum -> bool =
   fun projectee  ->
     match projectee with | Left _0 -> true | uu____344 -> false
 
-let __proj__Left__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Ap =
+let __proj__Left__item___0 : 'Ap 'Aq . ('Ap,'Aq) sum -> 'Ap =
   fun projectee  -> match projectee with | Left _0 -> _0
-let uu___is_Right : 'Ap 'Aq . ('Ap,'Aq) either -> bool =
+let uu___is_Right : 'Ap 'Aq . ('Ap,'Aq) sum -> bool =
   fun projectee  ->
     match projectee with | Right _0 -> true | uu____404 -> false
 
-let __proj__Right__item___0 : 'Ap 'Aq . ('Ap,'Aq) either -> 'Aq =
+let __proj__Right__item___0 : 'Ap 'Aq . ('Ap,'Aq) sum -> 'Aq =
   fun projectee  -> match projectee with | Right _0 -> _0
 type ('Ap,'Aq) l_or = unit
 type ('Ap,'Aq) l_imp = unit

diff --git a/ulib/prims.fst b/ulib/prims.fst
@@ -64,10 +64,10 @@ type bool : eqtype
     [False], see below. *)
 type empty = 
 
-(** [c_True] is the singleton inductive type---it is trivially
-    inhabited. Like [empty], [c_True] is seldom used. We instead use
+(** [trivial] is the singleton inductive type---it is trivially
+    inhabited. Like [empty], [trivial] is seldom used. We instead use
     its "squashed" variants, [True] *)
-type c_True = | T
+type trivial = | T
 
 (** [unit]: another singleton type, with its only inhabitant written [()]
     we assume it is primitive, for convenient interop with other languages *)
@@ -127,13 +127,13 @@ val smt_theory_symbol:attribute
 
 (** [l_True] has a special bit of syntactic sugar. It is written just
     as "True" and rendered in the ide as [True]. It is a squashed version
-    of constructive truth, [c_True]. *)
+    of constructive truth, [trivial]. *)
 [@@ "tac_opaque"; smt_theory_symbol]
-let l_True:logical = squash c_True
+let l_True:logical = squash trivial
 
 (** [l_False] has a special bit of syntactic sugar. It is written just
     as "False" and rendered in the ide as [Falsee]. It is a squashed version
-    of constructive truth, [c_True]. *)
+    of constructive falsehood, the empty type. *)
 [@@ "tac_opaque"; smt_theory_symbol]
 let l_False:logical = squash empty